proposition: Lemma ovaluation2_rev x: osuccp x -> ovaluation x = \0o.
proof: Proof. move => osx. move:(osx) =>[a oa av]. move:(olt0S oa); rewrite - av => xp. case: (ozero_dichot (OS_valuation xp)) => // vp. case:(limit_nonsucc' (ovaluation3 xp vp) osx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)