proposition: Lemma cnf_compare_nat_sum4 x y: cnfp_nz x -> cnfp_nz y -> oexp x \0c <o cnf_degree y -> x +f y <f x +#f y.
proof: Proof. move => xnz ynz lt1;move: (proj1 xnz) (proj1 ynz) => ox oy. split; first by apply: (cnf_compare_nat_sum2 ox oy). move => sv. move: (f_equal (Vr ^~(oexp x \0c)) sv). rewrite (cnf_nat_sum_p2 ox oy); move: (cnf_size_nz_ter xnz) => [qc qd]. have har: inc (Vg x \0c) (range x) by apply: (inc_V_range (proj41 ox) qc). rewrite (Vr_in_range ox har);set e := oexp x \0c. move/cnfpP:(ox) =>/proj43 h; move:(proj33 (h _ qc)) => [cN cp]; clear h. move:(nesym (proj2 cp)) => cnz. have os:= (cnfp_sum ox oy). case: (inc_or_not e (cnf_exponents (x +f y))). move/funI_P => [m md mv]. move: (NS_Vr e os); rewrite mv (Vr_in_range os md) => qN. case/(cnf_sum_rangeP ox ynz): md => mv1. - rewrite (Vr_in_range oy (proj1 mv1)) csumC. by move:(proj2 (csum_M0lt qN cnz)). - case: (proj2(olt_ltT lt1 (proj2 mv1))). by rewrite - (proj2(cnf_range_fgraph ox) _ _ har (proj1 mv1) mv). - by case: (proj2 lt1); rewrite - /e mv mv1; aw. move/Vr_oor => -> /esym /csum_nz; case => cz; by case:cp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)