proposition: Lemma Schutte_Cr_p5 a b: limit_ordinal a -> ordinalp b -> (Schutte_Cr a b <-> (forall c, c <o a -> Schutte_Cr c b)).
proof: Proof. move => ap ob; split. move => [x ox ->] c ca; exists (Sphi a x). apply: (OS_Sphi (proj32_1 ca) ox). by symmetry; apply: Sphi_p3. move /limit_ordinal_P: ap => [sa sb sc]. apply:Sphi_p4 => //. move => i ia; move:(sc _ (sb _ ia)) => [x ox xv]. move:(Sphi_p3 ox (oltS (proj31_1 ia))). by rewrite - xv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)