proposition: Lemma ord_compare_nat_sum4 x y: \0o <o x -> \0o <o y -> ovaluation x <o odegree y -> x +o y <o x +#o y.
proof: Proof. move => xp yp hyp. move: (proj32_1 xp) (proj32_1 yp) => ox oy. split; first by apply:ord_compare_nat_sum2. move: hyp. rewrite /ovaluation/odegree (Y_false (nesym (proj2 yp))) => h. move: (the_cnf_p0_nz xp) (the_cnf_p0_nz yp) => [oa av] [ob bv]. move: (proj2(cnf_compare_nat_sum4 oa ob h)). rewrite /natural_sum -(cnf_osum ox oy) => u v; case: u. move: (the_cnf_p0 (OS_sum2 ox oy)) => [qa qb]. apply: (cnf_val_inj qa (cnfp_nat_sum (proj1 oa) (proj1 ob))). by rewrite qb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)