proposition: Lemma natural_sum0 x : ordinalp x -> (x +#o \0o) = x.
proof: Proof. move => ox. move: (the_cnf_p0 ox) => [qa qb]. by rewrite /natural_sum the_CNF_0 cnf_nat_sum0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)