proposition: Lemma Schutte_Cr_p2 a: ordinalp a -> ordinalsf (Schutte_Cr a) =1o Sphi a.
proof: Proof. move => oa. have sa :=(Schutte_Cr_p1 oa). have sc := (ordinals_col_p2 sa). have sd := (Sphi_p1 oa). move: (ordinals_col_p1 (proj1 (proj1 sa)) (proj2 sa)) => [ha hb _ _ _]. apply: (sincr_ofs_exten (proj1 sc) (proj1 sd)) => x ox. exact (ha _ ox). by apply: hb; exists x. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)