proposition: Lemma odegree_of_monomial e c (x := oopow e *o c): ordinalp e -> posnatp c -> \0o <o x /\ odegree x = e.
proof: Proof. move => oe cp. have xp: \0o <o x. move/posnat_ordinalp: cp => [cp _]. apply: (oprod2_pos (oopow_pos oe) cp). split => //. rewrite (odegree_of_pos xp). rewrite (proj43 (cnf_one_term oe cp)) /oexp/cnf_size Lgd. rewrite LgV//; aw; trivial; rewrite cpred1; apply: (set1_1 \0c). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)