proposition: Lemma CNF_prod_pr2bis x: \0o <o x-> x *o omega0 = oopow (odegree x) *o omega0.
proof: Proof. move => [/proj32 ox /nesym xp]. move: (the_cnf_p0 ox)=> [ha hb]. have unz: the_cnf x <> emptyset by move => h;case: xp; rewrite - hb h cnf_val0. rewrite - hb (CNF_prod_pr2 (conj ha unz)). by rewrite /odegree hb (Y_false xp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)