proposition: Lemma cnf_compare_nat_sum2 x y: cnfp x -> cnfp y -> x +f y <=f x +#f y.
proof: Proof. move => ox oy. case: (equal_or_not y \0f) => ynz. by rewrite ynz cnf_sum0r (cnf_nat_sum0 ox); apply: (cnf_leR ox). move: (cnfp_nat_sum ox oy)(cnfp_sum ox oy) => os2 os1. apply: (cnf_le_prop os1 os2) => e. rewrite (cnf_nat_sum_p2 ox oy). case: (inc_or_not e (cnf_exponents (x +f y))) => h; last first. rewrite (Vr_oor h); apply: cle0x; fprops. move /funI_P: h => [z zr ->]. move:(CS_nat(NS_Vr (P z) os1)); rewrite (Vr_in_range os1 zr) => ov. case /(cnf_sum_rangeP ox (conj oy ynz)): zr. - by move => [qa _]; rewrite (Vr_in_range oy qa); apply:csum_Mle0. - by move => [qa _]; rewrite (Vr_in_range ox qa); apply:csum_M0le. - move => ->; aw; apply:cleR; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)