proposition: Lemma ord_compare_nat_sum3 x y: \0o <o x -> \0o <o y -> odegree y <=o ovaluation x -> x +o y = x +#o y.
proof: Proof. move => xp yp. move: (the_cnf_p0_nz xp) (the_cnf_p0_nz yp) => [oa av] [ob bv]. rewrite /ovaluation/odegree (Y_false (nesym (proj2 yp))) => h. rewrite /natural_sum - (cnf_compare_nat_sum3 oa ob h). move: (proj32_1 xp) (proj32_1 yp) => ox oy. by rewrite -(cnf_osum ox oy) (proj2 (the_cnf_p0 (OS_sum2 ox oy))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)