proposition: Lemma Spsi_p10 a: ordinalp a -> ~(normal_ofs (Spsi a)).
proof: Proof. move => oa [pa pb]. set x := Sphi (osucc a) \0o. case:(indecomp_limit (Schutte_Cr_p8' (OS_succ oa) OS0)). move: (oltS oa)=> lt1 e1. move: (Sphi_p3 OS0 lt1); rewrite e1 => e2. have ica:= (proj1 (Sphi_p1 oa)). move: (ica _ _ olt_01); rewrite e2;move/olt1 => e3. by move:(Schutte_Cr_p8' oa OS0) => [][]; rewrite e3. rewrite -/x => limx; move: (proj31 limx ) => ox. move:(Sphi_p1 oa)=> [pa' pb']. have pc: forall t, t<o x -> Sphi a t <> t. move => t tx eq. have ot:=proj31_1 tx. move: (oltS oa)=> lt1. move /(Schutte_Cr_p6 oa ot):(eq) => [y oy yb]. have : Sphi a t <o x. apply/(Sphi_p7 ot OS0 oa (OS_succ oa)); split => //. by move => e2; move: (proj2 lt1); rewrite - e2. by move /(oleNgt (proj1 lt1)). rewrite eq yb /x => eq2. case (ozero_dichot oy) => yz; first by move: (proj2 eq2); rewrite yz. case: (oltNge eq2 (proj1 (proj1 (Sphi_p1 (OS_succ oa)) _ _ yz))). have pd: forall t, t<o x -> Sphi a t = Spsi a t. move => t tx. rewrite /Spsi; Ytac H => //. move: H => [n [c [/proj31_1 on oc tv eq]]]. have cx: c<o x. apply: ole_ltT tx; rewrite tv; apply: osum_Mle0 => //. by case (pc _ cx). have: \osup (fun_image x (Sphi a)) = \osup (fun_image x (Spsi a)). by apply: ord_sup_2funI => t tx; apply: pd; apply /oltP. rewrite - (pb _ limx) - (pb' _ limx). move: (Sphi_p3 OS0 (oltS oa)); rewrite -/x => -> h. by move:(proj2 (Spsi_p2 oa ox)); rewrite - h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)