proposition: Lemma cnf_sum_rangeP x y: cnfp x -> cnfp_nz y -> forall t, inc t (range (x +f y)) <-> cnf_sum_monp x y (cnf_degree y) t.
proof: Proof. move => ox ynz; rewrite (cnf_sum_range ox ynz). exact: (cnf_sum_monP x y (cnf_degree y)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)