proposition: Lemma OS_degree x: ordinalp x -> ordinalp (odegree x).
proof: Proof. move => ox; rewrite /odegree; Ytac xz; first by apply: OS0. apply:(OS_degree_aux ole_2omega ox xz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)