proposition: Lemma natural_sumA a b c : ordinalp a -> ordinalp b -> ordinalp c -> a +#o (b +#o c) = (a +#o b) +#o c.
proof: Proof. move => oa ob oc. move: (the_cnf_p0 oa) => [qa qb]. move: (the_cnf_p0 ob) => [qa' qb']. move: (the_cnf_p0 oc) => [qa'' qb'']. rewrite /natural_sum. rewrite {1} (proj43(cnf_and_val_pb (cnfp_nat_sum qa' qa''))). rewrite (cnf_nat_sumA qa qa' qa''). by rewrite {1} (proj43(cnf_and_val_pb (cnfp_nat_sum qa qa'))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)