proposition: Lemma Spsi_cpc a a' b b': ordinalp b -> a' <o a -> Spsi a b <=o b' -> Spsi a b <o Spsi a' b'.
proof: Proof. move => ob pa pb. have [[oa' oa _] hh] := pa. have ob':= proj32 pb. apply/(Spsi_p12 oa oa' ob ob'); split => // ha; last by case: hh. case: (oltNge pa (proj1 ha)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)