proposition: Lemma Schutte_Cr_p4 a b: \0o <o a -> ordinalp b -> (Schutte_Cr a b <-> (forall c, c <o a -> Sphi c b = b)).
proof: Proof. move => ap ob; split. by move => [x ox ->] c ca; apply: Sphi_p3. by move /(Sphi_p4 ob ap). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)