proposition: Lemma cnfp_prod_gen x y : cnfp_nz x -> cnfp_nz y -> cnfp( cnf_prod_gen x y).
proof: Proof. move => xnz ynz. have [od1 od2]:= (cnf_size_nz_ter ynz). have ody: \1c <=c (domain y) by apply/cge1P. move/cnfpP:(proj1 ynz) =>[_ _ ew _ ]. move: (proj33 (ew _ od1))=> pny0 {ew}. 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. move: (cnfp_cnf_ns (proj1 ynz) ody) => or. move: (cnfp_shift_expo or (OS_cnf_degree xnz)) => oo. apply: (cnfp_cnf_nm cnk oo). move => i j. rewrite /cnf_nck /cnf_shift_expo 2! Lgd. have d1: domain (cnf_ns y \1c) = domain y -c \1c by rewrite/cnf_ns Lgd. move: (proj42 (proj1 xnz)) => dxN. move: (proj42 (proj1 ynz)) => dyN. move: (NS_diff \1c dyN); rewrite - d1 => dzN. move => idx jdy. move/(NltP dzN): (jdy); rewrite d1 => jiy. move/(NltP dxN): (idx) => iix; set u := oexp _ _. have -> : u = oexp x i by rewrite /u/oexp/cnf_c LgV//; Ytac foo;aw; trivial; rewrite foo. apply: (ole_ltT (cnf_degree_greatest (proj1 xnz) iix)). rewrite /oexp/cnf_ns/cnf_s !LgV//; aw. have od:= (OS_cnf_degree xnz). rewrite -{1} (osum0r od); apply:(osum_Meqlt _ od). move:(NS_lt_nat jdy dzN) => jN. have sjf: csucc j <c domain y. move: (cpred_pr dyN (nesym( proj2 od2)))=> [ha hb]. rewrite hb; apply/cltSS; rewrite (cpred_pr4 (proj32_1 od2)). by apply/NltP => //; rewrite - d1. move:(proj44 (proj1(proj44 (proj1 ynz))) j jN sjf). rewrite - (csucc_pr4 (proj31_1 jdy)) => h. exact:(ole_ltT (ole0x (proj31_1 h)) h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)