The first exponent of an ordinal
An ACL2 ordinal is either a natural number or, for an infinite
ordinal, a list whose elements are exponent-coefficient pairs (see o-p). In the latter case, this function returns the car of the first
pair in the list. In the case of a natural number, the value returned is
0 (since a natural number,
For the corresponding coefficient, see o-first-coeff.