proposition: Lemma ovaluation_prod a b: \0o <o a -> \0o <o b -> ovaluation (a *o b) = Yo (ovaluation b = \0o) (ovaluation a) (odegree a +o ovaluation b).
proof: Proof. move => ap bp. rewrite /ovaluation. rewrite (odegree_of_nz (nesym(proj2 ap))). move:(the_cnf_p0_nz ap) (the_cnf_p0_nz bp). set x := the_cnf a; set y := the_cnf b. move=> [xnz <-][ynz <-] . rewrite -/(cnf_degree x) -/(cnf_degree y). have dxN := (proj42 (proj1 xnz)). move: (cnf_size_nz xnz)(cnf_size_nz ynz) => [sxN sxv] [syN syv]. have [oody2 ody] := cnf_size_nz_ter ynz. move: (proj42(proj1 (proj44 (proj1 ynz))) \0c ody) => oox. have odx:=(OS_cnf_degree xnz). case: (ozero_dichot oox) => cz. rewrite (CNF_prod_pr6 xnz ynz cz). rewrite (proj43 (cnf_and_val_pb (cnfp_prod_gen xnz ynz))). rewrite/cnf_prod_gen/oexp/cnf_nm/cnf_shift_expo !Lgd. have ->: (domain y -c \1c) = cnf_size y. by rewrite syv - cpred_pr4; fprops; rewrite cpred_pr2. have [oodx2 oodx]:= cnf_size_nz_ter xnz. have aux: inc \0c (domain x +c cnf_size y). apply/(NltP (NS_sum dxN syN)). rewrite sxv(csum_Sn _ sxN); apply: succ_positive. rewrite LgV// /cnf_m; Ytac0; Ytac0; rewrite/cnf_nck /cnf_c. rewrite LgV//; Ytac foo => //; aw; ue. rewrite (CNF_prod_pr5 xnz ynz cz). rewrite (proj43 (cnf_and_val_pb (cnfp_shift_expo (proj1 ynz) odx))). by rewrite (Y_false (nesym (proj2 cz))) /oexp/cnf_shift_expo LgV//; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)