proposition: Lemma Spsi_p12 i j x y : ordinalp i -> ordinalp j -> ordinalp x -> ordinalp y -> (Spsi i x <o Spsi j y <-> [/\ i <o j -> x <o Spsi j y, i = j -> x <o y & j <o i -> Spsi i x <=o y]).
proof: Proof. move => oi oj ox oy. have aux: forall i' j' x' y', i' <o j' -> ordinalp x' -> ordinalp y' -> x' <o Spsi j' y' -> Spsi i' x' <o Spsi j' y'. move => i' j' x' y' pa ox' oy' sa. move: (pa) => [[oi' oj' _] _]. have: limit_ordinal (Spsi j' y'). apply:(Spsi_limit oj' oy'); left. move => jz; rewrite jz in pa; case: (olt0 pa). move/(limit_ordinal_P) => [_ h1]; move: (h1 _ sa) => h2. have ha:= (Spsi_p11 oi' ox'). move: (ole_ltT ha ((proj1 (Sphi_p1 oi') _ _ h2))). rewrite {2 4} /Spsi; set c := Yo _ _ _. have oc: ordinalp c by rewrite /c; Ytac h4; fprops. by rewrite (Sphi_p3 oc pa). case (oleT_ell oi oj) => ij. - have bad: i <o i -> False by move => []. rewrite - ij; split. move => h; split => h1; try (by case: bad). case: (oleT_ell ox oy) => // h2. by move: (proj2 h); rewrite h2. case: (oltNge h (proj1 (Spsi_p3 oi h2))). move => [_ h _]; exact: (Spsi_p3 oi (h (erefl i))). - split. move => h; split. + move => _; case (oleT_el (OS_Spsi oj oy) ox) => // h1. exact: (ole_ltT (proj1 (Spsi_p2 oi ox)) h). + by move => eq; move: (proj2 ij); case. + by move=> [/(oltNge ij)]. by move => [h _ _]; move: (h ij) => sa; by apply: aux. - split. move => h; split. + by move=> [/(oltNge ij)]. + by move => eq; move: (proj2 ij); case. + move => _. case (oleT_el (OS_Spsi oi ox) oy) => // h1. case: (oleNgt (proj1 (aux _ _ _ _ ij oy ox h1)) h). move => [_ _ h]; move: (h ij) => sa. exact: (ole_ltT sa (Spsi_p2 oj oy)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)