proposition: Lemma cnf_sum_small_deg x y: cnfp_nz x -> cnfp_nz y -> cnf_degree x <o cnf_degree y -> x +f y = y.
proof: Proof. move => xnz ynz cpd. move: (proj1 xnz) (proj1 ynz) => ox oy. apply:(cnf_same_range (cnfp_sum ox oy) oy). rewrite (cnf_sum_range ox ynz). have ha:=(cnf_size_nz_bis ynz). set d := (cnf_degree y). have hb i: inc i (domain x) -> oexp x i <o d. move => idx; exact: (ole_ltT (cnf_degree_greatest ox idx) cpd). have eq1: J d (Vr x d +c Vr y d) = Vg y (cnf_size y). case: (inc_or_not d (domain (range x))). move=> /funI_P [t /(range_gP (proj41 ox)) [i ia ->] iv]. by case:(proj2 (hb i ia)). move => h;rewrite {1}/Vr (Vg_out_of_range h). rewrite - (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. - move => [/ (range_gP (proj41 ox)) [i /hb /proj1 ok ->]]. by move/oltNge; case. - 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)