proposition: Lemma Spsi_p2' a b: ordinalp a -> ordinalp b -> a <=o Spsi a b.
proof: Proof. move => oa ob. have: indecomposable (Spsi a b). rewrite /Spsi; Ytac h; apply:Schutte_Cr_p8'; fprops. move/ (Spsi_p7) => [a' [b' [p1 p2 p3]]]. move: (Spsi_p4 oa (proj31 p1) ob (proj31_1 p2) p3). by move => [e1 e2]; rewrite {1} e1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)