proposition: Lemma Spsi_p7 x: indecomposable x -> (exists a b, [/\ a <=o x, b <o x & x = Spsi a b]).
proof: Proof. move => oix. move:(Sphi_p10b oix) => [a [b [pa pb pc]]]. move: (pb) => [[ob ox _] _]. case: (p_or_not_p (Spsi_aux a b)); last first. by move => h; exists a,b ; split => //; rewrite /Spsi; Ytac0. move => [n [c [oi oc pd pe]]]. have on:= proj31_1 oi. case: (ordinal_limA on) => nz. + have bc: b = c by move: pd; rewrite nz (osum0r oc). move: pe (proj2 pb); rewrite - bc - pc => -> //. + move: (predo_K nz); set m := opred n => sm. have om: ordinalp m by apply:OS_sup => t /(Os_ordinal on). have ocm:= OS_sum2 oc om. have le1: c +o m <o x. have: c +o m <=o c +o n. apply:osum_Meqle => //; rewrite - sm; exact: (proj1 (oltS om)). rewrite - pd => l2; exact:(ole_ltT l2 pb). have spa: (Spsi_aux a (c +o m)). exists m, c; split => //; move: (oltS om); rewrite sm=> h. exact (olt_ltT h oi). exists a, (c +o m); split => //;rewrite /Spsi; Ytac0. by rewrite osum2_succ // sm - pd. case:(oltNge oi (limit_ge_omega nz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)