proposition: Lemma OS_valuation x: \0o <o x -> ordinalp (ovaluation x).
proof: Proof. move => xp. apply: (proj42(proj1 (proj44 (proj1 (the_cnf_p0 (proj32_1 xp)))))). rewrite (proj2(the_cnf_p2 xp)); apply: succ_positive. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)