proposition: Lemma Schutte_Cr_p8' a b: ordinalp a -> ordinalp b -> indecomposable (Sphi a b).
proof: Proof. by move => oa ob; apply (Schutte_Cr_p8 oa (OS_Sphi oa ob)); exists b. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)