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