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