proposition: Lemma maximal_criticalP a x: ordinalp a -> ordinalp x -> (maximal_critical a x <-> exists2 b, b<o x & x = Sphi a b).
proof: Proof. move => oa ox; split. move=> [[c oc cv] pb]; exists c => //. have ica:= (proj1 (Sphi_p1 oa)). move:(osi_gex ica oc); rewrite - cv => cx; split => // ecx. rewrite ecx in cv. by case:(pb _ (oltS oa)); apply/(Schutte_Cr_p6 oa ox). move => [b bx bv]; split; first by exists b => //; exact (proj31_1 bx). move => c ac [d od dv]. rewrite dv in bv. move/(Sphi_p6 od (proj31_1 bx) (proj32_1 ac) oa): bv. by move => [_ _ h]; move: (h ac) (proj2 bx); rewrite - dv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)