proposition: Lemma Spsi_p3 a b b': ordinalp a -> b <o b' -> (Spsi a b <o Spsi a b').
proof: Proof. move => oa bb'; rewrite /Spsi. have sbb: osucc b <o osucc b' by move /oltSSP: bb'. apply: (proj1 (Sphi_p1 oa)). Ytac pa; Ytac pb => //. split; first by move/oleSltP: bb'. move => h; move: pa => [n [c [qa qb qc qd]]]; case: pb. exists (osucc n), c; split => //. by move: omega_limit => /limit_ordinal_P [_]; apply. rewrite -h qc osum2_succ //; exact (proj31_1 qa). exact:(olt_ltT bb' (oltS (proj32_1 bb'))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)