proposition: Lemma cnf_valuation_sum_spec x y: cnfp x -> cnfp y -> domain y = \1c -> oexp (x +f y) \0c = oexp y \0c.
proof: Proof. move => ox oy dy1. have sy: cnf_size y = \0c by rewrite /cnf_size dy1 cpred1. set d := oexp y \0c. have dd: d = cnf_degree y by rewrite/cnf_degree sy. have ynz: cnfp_nz y. split => //;move => yz; move: dy1; rewrite yz domain_set0; fprops. have xynz : x +f y <> emptyset by apply: cnf_sum_nz. move:(cnfp_sum ox oy) => os. have H := cnf_sum_rangeP ox ynz. have zdd: inc \0c (domain (x +f y)). apply/(NltP (proj42 os)); apply: (card_ne0_pos (CS_nat (proj42 os))). by move/domain_set0_P. apply: oleA. set t := J d (Vr x d +c Vr y d). have: inc t (range (x +f y)) by rewrite /t dd; apply/H; constructor 3. move=> /(range_gP (proj41 os)) [i idx iv]. move/(NltP (proj42 os)): idx => ily. move: (cle0x (proj31_1 ily)) => i0. move:(CNF_exponents_M (proj42 os) (proj1 (proj44 os)) i0 ily). by rewrite /oexp - iv /t pr1_pair. move:(inc_V_range (proj41 os) zdd); rewrite /oexp; set u := Vg _ _. case /H. - move => [/(range_gP (proj41 oy)) [i idy idv]/oltNge pv]. move/(NltP (proj42 oy)): idy => ily. move: (cle0x (proj31_1 ily)) => i0. case: pv; rewrite idv - dd. exact(CNF_exponents_M (proj42 oy) (proj1 (proj44 oy)) i0 ily). - by move => [_ /proj1]; rewrite dd. - by move ->; rewrite pr1_pair dd; apply: oleR; apply: OS_cnf_degree. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)