proposition: Lemma CNF_prod_pr1 x k : cnfp_nz x -> posnatp k -> (cnf_val x) *o k = cnf_val (cnf_nck x k).
proof: Proof. move => xnz pnk. move: (OS_cnf_val (proj1 xnz)) => oox. move:(posnat_lc xnz) => pnlc. move:pnk => [kN kp]. move: (cpred_pr kN (nesym (proj2 kp))) => [nN ->]. move: (cpred k) nN; clear kN kp; apply: Nat_induction. by rewrite succ_zero (oprod1r oox) (cnf_nck_prop2 xnz). move => n nN Hr. move: (NS_succ nN) => snN. have eq1 := (succ_of_nat snN). rewrite eq1 (oprod2_succ (OS_cnf_val (proj1 xnz)) (OS_nat snN)) Hr - eq1. set y := (cnf_nck x (csucc n)). have hu: domain y = domain x by rewrite /y/cnf_nck Lgd. have hv := (cnf_size_nz_bis xnz). have sd: cnf_degree (cnf_nck x (csucc n)) = cnf_degree x. rewrite /cnf_degree/cnf_size hu /cnf_nck/oexp LgV//. by rewrite /cnf_c/cnf_size; Ytac0; aw. have hw: (cnf_lc y) = (cnf_lc x *c csucc n). rewrite /cnf_lc /cnf_size hu /y /cnf_nck /ocoef LgV //. by rewrite /cnf_c/cnf_size; Ytac0; aw. have ynz: y <> emptyset. by move => /domain_set0_P; rewrite hu => /domain_set0_P/(proj2 xnz). have oy := (cnf_nck_prop3 xnz nN). rewrite (CNF_sum_pr3 (conj oy ynz) xnz sd). by rewrite (cnf_nck_prop1 _ snN) - hw; reflexivity. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)