proposition: Lemma cnf_nm_sum x y: cnfp x -> cnfp y -> cnf_all_smaller x y -> (cnf_nm x y) = y +f x.
proof: Proof. move => ox oy cpd. move: (cnfp_cnf_nm ox oy cpd) => oz. apply: (cnf_same_range oz (cnfp_sum oy ox)). rewrite (cnfp_cnf_nm_range ox oy). case: (equal_or_not x emptyset) => xz. by rewrite /cnf_sum xz range_set0 (Y_true (erefl _)) setU2_C setU2_0. have xnz := conj ox xz. move: (ox) => [fgx nN _ _]. move: (oy) => [fgy mN _ _]. move: (cnf_size_nz xnz) => [qa qb]. have sxdx:= (cnf_size_nz_bis xnz). move/(NltP nN): (sxdx) => sxix. have prop1: Vr y (cnf_degree x) = \0c. apply:Vg_out_of_range; move/funI_P => [z /(range_gP fgy) [i idy ->]] . move/(NltP mN): idy => pb. exact:(proj2 (cpd (cnf_size x) i sxix pb)). have prop2: Vg x (cnf_size x) = J (cnf_degree x) (Vr y (cnf_degree x) +c Vr x (cnf_degree x)). rewrite - (proj43 ox _ sxdx); apply: f_equal. rewrite prop1 - (cnf_coef_of_lc xnz) csum0l //. exact:(CS_nat (proj1 (posnat_lc xnz))). set_extens t. move => tp; apply/(cnf_sum_rangeP oy xnz). case/setU2_P:tp => trx. move/(range_gP fgx): (trx) => [i idx mv]. move/(NltP nN): idx; rewrite qb; move/(cltSleP qa). case/cle_eqVlt => ha; first by constructor 3; rewrite mv ha. constructor 1; split; first exact. by rewrite mv;exact:(cnf_degree_greatest_bis ox ha). constructor 2; split; first exact. move/(range_gP fgy): (trx) => [i idx ->]; apply: (cpd _ _ sxix). by apply/NltP. case/(cnf_sum_rangeP oy xnz). - by move => [ha _]; apply:setU2_1. - by move => [ha _]; apply:setU2_2. - by rewrite - prop2 => ->; apply:setU2_1; apply: inc_V_range. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)