proposition: Lemma CNFp_pr1 e c: \0o <o e -> posnatp c -> CNFp_value1 e c = CNFp_value2 e c.
proof: Proof. move=> ep cp. move: (CS_nat (proj1 cp)) => cz. rewrite /CNFp_value1 /CNFp_value2. move:(CNF_succ_pow ep); set v := variantLc _ _; set x := osucc _. move => [qa qb qc qd]. have vnz: cnfp_nz v by split=> //; move/domain_set0_P;rewrite /v;aww. rewrite - qd (CNF_prod_pr1 vnz cp) - (proj44 (CNF_succ_pow1 ep cp)). congr cnf_val;rewrite /cnf_nck/v /cnf_size/cnf_c; aw; rewrite cpred2. have foo: ~(C0 = \1c) by fprops. apply: Lg_exten => y yd; try_lvariant yd; first by Ytac0. rewrite/cnf_degree/cnf_lc/ocoef/cnf_size/oexp (Y_true (erefl C1)); aw. by rewrite cpred2 LgV//; aww; rewrite cprod1l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)