proposition: Lemma ord_compare_nat_sum2 x y: ordinalp x -> ordinalp y -> x +o y <=o x +#o y.
proof: Proof. move => ox oy. move: (the_cnf_p0 ox) (the_cnf_p0 oy) => [oa av] [ob bv]. move: (the_cnf_p0 (OS_sum2 ox oy)) => [ixy]. rewrite /natural_sum (cnf_osum ox oy) => <-. apply/(cnf_le_compat (cnfp_sum oa ob) (cnfp_nat_sum oa ob)). apply:(cnf_compare_nat_sum2 oa ob). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)