proposition: Lemma odegree_infinite x : omega0 <=o x -> \0o <o odegree x.
proof: Proof. move => xo. case: (ozero_dichot (OS_degree (proj32 xo))) => oz //. move: (proj2(the_cnf_p4 (olt_leT olt_0omega xo)));rewrite oz osucc_zero oopow1. by move/oltNge. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)