proposition: Lemma CNF_prod_pr6 x y: cnfp_nz x -> cnfp_nz y -> oexp y \0c = \0o -> (cnf_val x) *o (cnf_val y) = cnf_val (cnf_prod_gen x y).
proof: Proof. move => xnz ynz vz. have [od2 od1] := cnf_size_nz_ter ynz. have ody: \1c <=c (domain y) by apply/cge1P. move: (proj44 (proj1 ynz)) => [[_ qb qc _] _]. move: (proj31_1 (qc _ od1)) (OS_cnf_val (proj1 xnz)) => ra rb. move/cnfpP:(proj1 ynz) =>[_ _ ew _ ]. move: (proj33 (ew _ od2))=> pny0 {ew}. move: (cnfp_cnf_ns (proj1 ynz) ody) => or. rewrite (cnf_sum_rec ynz) vz oopow0 (oprod1l ra). rewrite (oprodD (OS_cnf_val or) ra rb). have cnk: cnfp(cnf_nck x (ocoef y \0c)). move:pny0 =>[ua ub];move: (cpred_pr ua (nesym (proj2 ub)))=> [uc ud]. by rewrite /ocoef ud; apply:cnf_nck_prop3. rewrite(CNF_prod_pr1 xnz pny0). have aux t: cnfp t -> cnf_nm t emptyset = t. move => [ha hb hc hd]; rewrite/cnf_nm domain_set0 (csum0r (CS_nat hb)). apply: fgraph_exten; aww => i idt; rewrite LgV//. by rewrite/cnf_m Y_true//; apply/(NltP hb). case: (equal_or_not (domain y) \1c) => dy1. have eq0:(cnf_ns y \1c) = emptyset. by rewrite/cnf_ns dy1 cdiff_nn /Lg funI_set0. rewrite /cnf_prod_gen eq0 cnf_val0 oprod0r (osum0l (OS_cnf_val cnk)). by rewrite /cnf_shift_expo domain_set0 /Lg funI_set0 (aux _ cnk). have qd: \1c <c domain y by split; fprops. have dsnz: (domain y -c \1c) <> \0c by apply: cdiff_nz. have cys: cnfp_nz (cnf_ns y \1c). by split =>// /domain_set0_P ;rewrite /cnf_ns Lgd. have nep: \0o <o oexp (cnf_ns y \1c) \0c. have qe: inc \0c (domain y -c \1c). apply/(NltP (NS_diff \1c (proj42(proj1 ynz)))). by apply: (card_ne0_pos (CS_diff _ _)). rewrite - vz /oexp /cnf_ns/cnf_s LgV// (csum0l CS1) - succ_zero. have qf: csucc \0c <c domain y by rewrite succ_zero. by move:(proj44(proj1 (proj44(proj1 ynz))) _ NS0 qf). rewrite (@CNF_prod_pr5 x (cnf_ns y \1c) xnz cys nep). rewrite cnf_sum_prop1 //; apply: (cnfp_shift_expo or (OS_cnf_degree xnz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)