proposition: Lemma cnf_osum x y: ordinalp x -> ordinalp y -> the_cnf (x +o y) = the_cnf x +f the_cnf y.
proof: Proof. move => ox oy. move: (the_cnf_p0 ox)(the_cnf_p0 oy); set a := the_cnf x; set b := the_cnf y. move => [oa av][ob bv]. move: (cnf_sum_compat_prop oa ob). rewrite /cnf_sum_compat av bv. move <-. exact: (proj43 (cnf_and_val_pb (cnfp_sum oa ob))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)