proposition: Lemma cnf_compare_nat_sum1 x y: cnfp x -> cnfp y -> x <=f x +#f y.
proof: Proof. move => ox oy; apply: (cnf_le_prop ox (cnfp_nat_sum ox oy))=> e. rewrite (cnf_nat_sum_p2 ox oy); apply: (csum_M0le _ (CS_nat (NS_Vr e ox))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)