proposition: Lemma Spsi_indecomposable a b: ordinalp a -> ordinalp b -> indecomposable (Spsi a b).
proof: Proof. move => oa ob. rewrite /Spsi;apply:(Schutte_Cr_p8' oa); Ytac h=> //; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)