proposition: Lemma odegree_opow n:ordinalp n -> odegree (oopow n) = n.
proof: Proof. move => oe; rewrite (odegree_of_pos (oopow_pos oe)). rewrite (proj43 (cnf_singleton1 oe)) /oexp/cnf_size Lgd. rewrite LgV// ?cpred1;aw; trivial; apply: (set1_1 \0c). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)