proposition: Lemma cnf_sum_range x y: cnfp x -> cnfp_nz y -> range (x +f y) = cnf_sum_mons x y (cnf_degree y).
proof: Proof. move => ox ynz. rewrite /cnf_sum (Y_false (proj2 ynz)). by rewrite (proj2 (cnf_sort_correct (cnf_sum_mon_range ox ynz))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)