proposition: Lemma ovaluation2 x: \0o <o x -> ovaluation x = \0o -> osuccp x.
proof: Proof. move => xp vz; move: (ovaluation1 xp) => [y oy ->]. rewrite vz oopow0 (osucc_pr oy); exists y => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)