proposition: Lemma Schutte_Cr_p6 a b: ordinalp a -> ordinalp b -> (Schutte_Cr (osucc a) b <-> Sphi a b = b).
proof: Proof. move => oa ob. have osa := OS_succ oa. have sa: \0o <o osucc a by apply: ord_ne0_pos => //;apply: osucc_nz. have asa:= (oltS oa). split; first by move/(Schutte_Cr_p4 sa ob) => h; exact: (h a asa). move => aux. apply/(Schutte_Cr_p4 sa ob) => c /oltSleP ca. case: (equal_or_not c a) => eca; first by rewrite eca. by rewrite - aux; apply: Sphi_p3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)