proposition: Lemma ord_compare_nat_sum5 x y z: ordinalp x -> ordinalp y -> ordinalp z -> (x +#o z <=o y +#o z <-> x <=o y).
proof: Proof. move => ox oy oz. move: (the_cnf_p0 ox) (the_cnf_p0 oy) => [oa av] [ob bv]. move: (the_cnf_p0 oz) => [oc cv]. move: (cnf_le_compat oa ob); rewrite av bv => H1; apply: iff_trans H1. rewrite /natural_sum. move: (cnf_le_compat (cnfp_nat_sum oa oc) (cnfp_nat_sum ob oc)) => H2. by apply: (iff_trans (iff_sym H2)); apply: cnf_compare_nat_sum5. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)