proposition: Lemma OS_natural_sum x y : ordinalp x -> ordinalp y -> ordinalp (x +#o y).
proof: Proof. move => ox oy. move: (the_cnf_p0 ox) (the_cnf_p0 oy) => [qa qb][qc qd]. exact: (OS_cnf_val(cnfp_nat_sum qa qc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)