proposition: Lemma cnf_sum0l y: cnfp y -> \0f +f y = y.
proof: Proof. move => oy. case: (equal_or_not y emptyset) => yz; first by rewrite /cnf_sum; Ytac0. have ynz := (conj oy yz). apply:(cnf_same_range (cnfp_sum cnfp0 oy) oy). rewrite (cnf_sum_range cnfp0 ynz). have ha := (cnf_size_nz_bis ynz). set d := (cnf_degree y). have eq1: J d (Vr C0 d +c Vr y d) = Vg y (cnf_size y). rewrite cnf_coef_or_e_zero - (cnf_coef_of_lc ynz). by rewrite (csum0l (CS_nat (proj1 (posnat_lc ynz)))) (proj43 oy _ ha). set_extens t. move/cnf_sum_monP; case. - by case. - by case; rewrite range_set0 => /in_set0. - rewrite eq1 => ->; apply: (inc_V_range (proj41 oy) ha). move => tr; apply/ cnf_sum_monP. move/(range_gP (proj41 oy)): (tr) => [i idy tv]. move: (cnf_size_nz ynz) => [hc hd]. move: idy; rewrite hd => /(NleP hc) => /cle_eqVlt; case. by move=> iv; constructor 3; rewrite eq1 - iv. by move/(cnf_degree_greatest_bis oy); rewrite /oexp - tv => he; constructor 1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)