proposition: Lemma Schutte_Cr_p9 x y: ordinalp x -> ordinalp y -> Schutte_Cr x y -> x <=o y.
proof: Proof. move => ox oy [z oz ->]. move: (Sphi_p9 ox) => h. case (ozero_dichot oz) => eq; first by rewrite eq. by move: (proj1 (Sphi_p1 ox) _ _ eq) => [/(oleT h) le _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)