proposition: Lemma cnf_nat_sum_p2 x y : cnfp x -> cnfp y -> forall e, Vr (x +#f y) e = (Vr x e) +c Vr y e.
proof: Proof. move => ox oy e. move:(cnf_sort_correct (cnf_nat_sum_range ox oy)). rewrite/cnf_nat_sum; set z := cnf_sort _; move => [oz rz]. have dz: domain (range z) = domain (range x) \cup (domain (range y)). rewrite rz /cnf_nat_sum_mons; set_extens t. by move/funI_P =>[i /funI_P[j ja ->] ->]; aw. move => ta; apply /funI_P. exists (J t (Vr x t +c Vr y t)); aw; trivial. by apply/funI_P; ex_tac. case: (inc_or_not e (domain (range z))) => iE; last first. case: (inc_or_not e (domain (range x))) => edx. by case iE; rewrite dz; apply: setU2_1. case: (inc_or_not e (domain (range y))) => edy. by case iE; rewrite dz; apply: setU2_2. by rewrite (Vr_oor iE) (Vr_oor edx) (Vr_oor edy) (csum0l CS0). set w := RHS; have pp: inc (J e w) (range z). by rewrite rz;apply/funI_P;exists e => //; rewrite - dz. by rewrite (pr2_def(in_graph_V (cnf_range_fgraph oz) pp)); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)