proposition: Lemma cnf_nat_sum_range x y: cnfp x -> cnfp y -> cnf_rangep (cnf_nat_sum_mons x y).
proof: Proof. move => ox oy. have ha: finite_set (cnf_nat_sum_mons x y). have aux z: cnfp z -> finite_set (cnf_exponents z). move => [ha hb _ _]. apply/finite_fun_image; apply: (finite_range ha). apply:(finite_set_nat hb). apply: finite_fun_image; apply: (setU2_finite (aux _ ox) (aux _ oy)). have hb: sgraph (cnf_nat_sum_mons x y). move => t /funI_P [i ii ->]; fprops. have hc: fgraph (cnf_nat_sum_mons x y). split; [exact | move => t j /funI_P [a ii ->] /funI_P [b ji ->]]. by rewrite 2! pr1_pair => ->. split => // i /funI_P [a ii ->]; case/setU2_P: ii. move/funI_P => [z zr zv]. move/(range_gP (proj41 ox)): zr => [k kdx kv]. rewrite {1 2} zv kv -/(oexp x k) (Vr_correct ox kdx). move /cnfpP:(ox) =>/proj43 => mn; move: (mn _ kdx)=> [qa qb qc]. split;aww; rewrite csumC. apply: (posnat_add (NS_Vr a oy) qc). move/funI_P => [z zr zv]. move/(range_gP (proj41 oy)): zr => [k kdx kv]. rewrite {1 3} zv kv -/(oexp y k) (Vr_correct oy kdx). move /cnfpP:(oy) =>/proj43 => mn; move: (mn _ kdx)=> [qa qb qc]. split;aww;apply: (posnat_add (NS_Vr a ox) qc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)