proposition: Lemma cnfp_sum x y: cnfp x -> cnfp y -> cnfp (x +f y).
proof: Proof. move => ha hb. rewrite /cnf_sum; Ytac h => //. exact: (proj1 (cnf_sort_correct (cnf_sum_mon_range ha (conj hb h)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)