proposition: Lemma Spsi_p0 a: ordinalp a -> Spsi a \0o = Sphi a \0o.
proof: Proof. move => oa; rewrite /Spsi; Ytac h => //. move: h => [n [c [on oc eq1]]]. move: (osum2_zero oc (proj31_1 on) (sym_eq eq1)) => [-> _] eq2. by move:(proj2(proj1 (Schutte_Cr_p8' oa OS0))); rewrite eq2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)