proposition: Lemma odegree_succ_pow n : \0o <o n -> odegree (osucc (oopow n)) = n.
proof: Proof. move => h. rewrite (odegree_of_nz (@osucc_nz _)). move: (CNF_succ_pow h) => [_ _ -> _]. by rewrite /cnf_size /oexp; aw; rewrite cpred2; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)