proposition: Lemma ovaluation3_rev x: limit_ordinal x -> \0o <o x /\ \0o <o ovaluation x.
proof: Proof. move => lx; move:(limit_pos lx) => xp; split => //. case: (ozero_dichot (OS_valuation xp)) => vp //. case: (limit_nonsucc' lx (ovaluation2 xp vp)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)