proposition: Lemma cnf_nat_sumC x y: x +#f y = y +#f x.
proof: Proof. rewrite /cnf_nat_sum/cnf_nat_sum_mons setU2_C. by apply: f_equal; apply: funI_exten => a _; rewrite csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)