proposition: Lemma Sphi_p10b x: indecomposable x -> (exists a b, [/\ a <=o x, b <o x & x = Sphi a b]).
proof: Proof. move => ix; move: (ix) => [xp _]. have ox:= proj32_1 xp. have sa:= (proj1 (Sphi_p1 ox) _ _ xp). have sb:= (ole_ltT (Sphi_p9 ox) sa). pose p a:= Sphi a x = x. have npa: not (p x) by move => h; move: sb => []; rewrite h. move: (least_ordinal3 ox npa (p := p)). set a := least_ordinal _ x; move => [oa nn etc]. case: (oleT_el oa ox); [move => ax | by move => /etc px]. have [b ob xv]: exists2 b, ordinalp b & x = Sphi a b. case: (ozero_dichot oa) => az. by rewrite az;move/(Schutte_Cr_p3 ox): ix. apply:(Sphi_p4 ox az etc). have ica := (proj1 (Sphi_p1 oa)). have xaxx := (osi_gex ica ox). have h: x <o Sphi a x by split => // eq; case nn. exists a,b ; split => //. case: (oleT_ell ox ob). + by move => eq; move: (proj2 h); rewrite {2} eq. + by move => xb; case: (oltNge h); move: (proj1(ica _ _ xb)); rewrite - xv. + done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)