proposition: Lemma cnf_compare_nat_sum3 x y: cnfp_nz x -> cnfp_nz y -> cnf_degree y <=o oexp x \0c -> x +f y = x +#f y.
proof: Proof. move => xp yp mt1. move: (proj1 xp) (proj1 yp) => ox oy. move: (cnfp_nat_sum ox oy)(cnfp_sum ox oy) => os2 os1. apply: (cnf_nat_sum_p3 ox oy os1) => e. set Ha := (cnf_sum_rangeP ox yp). case: (inc_or_not e (cnf_exponents x)) => eex. move: (CS_nat(NS_Vr e ox)). move/funI_P:eex =>[m mr ->]. move/(range_gP (proj41 ox)):(mr) => [i idx iv]. move/(NltP (proj42 ox)): idx => ilx. move: (cle0x (proj31_1 ilx)) => ip. move: (CNF_exponents_M (proj42 ox) (proj1(proj44 ox)) ip ilx) => la. move: (oleT mt1 la); case /ole_eqVlt => lv. have: inc (J (P m) (Vr x (P m) +c Vr y (P m))) (range (x +f y)). by apply/Ha; constructor 3; rewrite iv lv. by move/(Vr_in_range os1); aw. have: inc (Vg x i) (range (x +f y)). by apply/Ha; constructor 2; rewrite -{1} iv. rewrite (Vr_in_range ox mr) iv; move/(Vr_in_range os1) => -> cc. case: (inc_or_not (oexp x i) (cnf_exponents y)). move/funI_P => [mm /(range_gP (proj41 oy)) [j jdy jv] mmv]. by case: (proj2 (ole_ltT (cnf_degree_greatest oy jdy) lv)); rewrite mmv jv. by move/Vr_oor => ->; by rewrite (csum0r cc). move: (cnf_size_nz yp) => [nN nv]. have he: inc (cnf_size y) (domain y) by rewrite nv; apply: Nsucc_i. have hc: inc (Vg y (cnf_size y)) (range y). by apply/(range_gP (proj41 oy)); ex_tac. case: (inc_or_not e (cnf_exponents y)) => eey. move/funI_P:eey =>[m mr -mv]. move/(range_gP (proj41 oy)):(mr) => [i idy iv]. move/(NltP (proj42 oy)): (idy); rewrite nv => /(cltSleP nN). case /(cle_eqVlt) => isy. have: inc (J e ((Vr x e) +c Vr y e)) (range (x +f y)). by apply/Ha; constructor 3; rewrite mv iv isy. by move/(Vr_in_range os1); aw. move: (cnf_degree_greatest_bis oy isy) => l1. have mr1 : (inc m (range (x +f y))). by apply/Ha;constructor 1; split => //; rewrite iv. rewrite (Vr_oor eex) (csum0l (CS_nat(NS_Vr e oy))). by rewrite mv (Vr_in_range os1 mr1) (Vr_in_range oy mr). rewrite (Vr_oor eex) (Vr_oor eey) (csum0l CS0). case: (inc_or_not e (cnf_exponents (x +f y))) => eez; last by rewrite Vr_oor. move: eex eey; move:eez => /funI_P [z /Ha ze ->]; case: ze. - by move => [zy _]; move => _; case; apply/funI_P; ex_tac. - by move => [zy _]; case; apply/funI_P; ex_tac. - by move => -> _; aw; case; apply/funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)