proposition: Lemma ord_compare_nat_sum1 x y: ordinalp x -> ordinalp y -> x <=o x +#o y.
proof: Proof. move => ox oy. move: (the_cnf_p0 ox) (the_cnf_p0 oy) => [oa av] [ob bv]. rewrite /natural_sum - {1} av. apply/(cnf_le_compat oa (cnfp_nat_sum oa ob)). by apply:cnf_compare_nat_sum1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)