proposition: Lemma odegree_finite x : x <o omega0 -> odegree x = \0o.
proof: Proof. move => xo. case: (ozero_dichot (proj31_1 xo)) => xp; first by rewrite xp odegree_zero. case: (ozero_dichot (OS_degree (proj31_1 xo))) => dp //. case: (oltNge (ole_ltT (proj1 (the_cnf_p4 xp)) xo)). by move/oge1P: dp => /opow_Mo_le; rewrite oopow1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)