proposition: Lemma ovaluation_sum a b: ordinalp a -> \0o <o b -> ovaluation (a +o b) = ovaluation b.
proof: Proof. move => oa bp. move: (ovaluation1 bp) => [c oc ->]. move:(OS_valuation bp) => ov. rewrite (osumA oa oc (OS_oopow ov)). by rewrite (ovaluation4 (OS_sum2 oa oc) ov) (ovaluation4 oc ov). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)