proposition: Lemma all_der_p13 : f \0o <> \0o -> normal_ofs (g \0o).
proof: Proof. move => fz. have pa: forall i j, i <o j -> g \0o i <o g \0o j. move => i j ij;move:(ij)=> [[oi oj _] _]. apply/(all_der_p10 OS0 OS0 oi oj); split => //. + move => _; apply: ord_ne0_pos; first by apply:(OS_all_der OS0 oj). move => eq1; move:(all_der_p7 OS0 (ole_ltT (ole0x oi) ij)). by rewrite eq1 (all_der_p2 OS0). + by move: (proj2 ij). + by move => [/(oltNge ij)]. split => // j lj. move: lj => [oj z0j lj1]. have osi: ordinal_set (fun_image j (g \0o)). move => t /funI_P [i ij ->]; apply:OS_all_der; fprops. exact: (Os_ordinal oj ij). have oy: (ordinalp (g \0o j)) by apply:OS_all_der; fprops. have ubb: ordinal_ub (fun_image j (g \0o)) (g \0o j). move => t /funI_P [i ij ->]. have ij1: i <o j by apply/(oltP oj). exact (proj1 (pa _ _ ij1)). set ww := \osup (fun_image j (g \0o)). pose Tk k := (fun_image (Zo j (fun z => k <o z)) (g \0o)). have wa: forall k, k <o j -> inc (g \0o (osucc k)) (Tk k). move => k kj. have ikj: inc k j by apply/oltP. move:(lj1 _ ikj) => kj1. apply/funI_P; exists (osucc k) => //; apply/Zo_P; split => //. apply: (oltS (proj31_1 kj)). have pc: forall k, k <o j -> \osup (Tk k) = ww. move => k kj. apply: ord_sup_1cofinal => //; split. move => t /funI_P [z /Zo_S zj ->]; apply/funI_P; ex_tac. move => x /funI_P [z zj ->]. move: (Os_ordinal oj zj) (proj31_1 kj) => oz ok. case (oleT_el oz ok) => kz. exists (g \0o (osucc k)); first by exact:(wa _ kj). by move /oltSleP: kz => /pa []. exists (g \0o z); first by apply/funI_P; exists z => //;apply/Zo_P. apply: oleR; apply:OS_all_der; fprops. move: (all_der_bound_prop OS0 oj bf). set C:= union _; set E:= cnext C. move => [sa sb sc sd se]. rewrite sd in sb sc se. move: (all_der_bound_prop2 OS0 oj); rewrite sd => sf. move:(many_der_ex sa sf); rewrite -/E. set ff:= (many_der (Lf f E E) E). pose ii i:= (intersectionf i (fun z : Set => fixpoints (Vf ff z))). move=> [ua ub uc _ [_ _ ug uh]]. have oe:= proj1(CS_cnext (proj1 sa)). have lje: j <o E by apply/(oltP oe). have wwe: inc ww E. have p1:sub (fun_image j (g \0o)) E. move => t /funI_P [z za ->]. have ze:=(ordinal_transitive oe sc za). move: (ug _ ze) => [[fg sg tg] _ _]. rewrite (all_der_p1 sa sb ze se). rewrite -tg -/E /all_der_aux -/ff; Wtac. apply: cnext_sup => //. move/(cnextP (proj1 sa)):sc => [_ rd]. exact: (cleT (fun_image_smaller j (g \0o)) rd). have pd: forall k, k<o j -> ww = g ww k. move => k kj; rewrite - (pc _ kj). have pr1: forall x, inc x (Tk k) -> x = g x k. move => x /funI_P [i /Zo_P [va vb] eq]. by move: (all_der_p7 OS0 vb); rewrite - eq. set Z:= fun_image (Tk k) (g^~k). have h1: Tk k = Z. set_extens t. move => tk; move:(pr1 t tk) => eq1; apply/funI_P; ex_tac. by move => /funI_P [z za zb]; move: (pr1 _ za); rewrite - zb => <-. have nez: nonempty Z by rewrite - h1; move: (wa _ kj) => h; ex_tac. have h2: forall x, inc x Z -> \0o <=o x. rewrite -h1; move => x /funI_P [i /Zo_P[ta tb] ->]. exact: (ole0x (OS_all_der OS0 (proj32_1 tb))). move: (all_der_p6 (proj31_1 kj)) => na. move/normal_ofs_equiv1: na => [_ h3]. by move: (h3 _ h2 nez); rewrite - h1 -/Z - h1. have pe: inc ww (Imf (Vf ff j)). have nej: nonempty j by ex_tac. case:(equal_or_not j \0o) => jnz; first by move: z0j; rewrite jnz;case;case. rewrite (uh _ sc jnz); apply/setIf_P => // k kj. have lkj: k <o j by apply/(oltP oj). have ke:= (olt_i(olt_leT lkj (proj1 lje))). move: (ug _ ke) => [[va vb vc] _ _ ]. have eq1: Vf (Vf ff k) ww = ww. by symmetry;rewrite {1} (pd _ lkj) (all_der_p1 sa wwe ke se). by apply/Zo_P; rewrite vb. move: (ug _ sc) => [[va vb vc] _ _ ]. move /(Imf_P va): pe; rewrite vb; move => [u ue eq2]. have eq3: ww = g u j by rewrite (all_der_p1 sa ue sc se) eq2. move: (ord_ub_sup oy ubb);rewrite -/ww eq3 => h. case: (equal_or_not u \0o) => uz; first by rewrite uz. have luz:=(ord_ne0_pos (Os_ordinal oe ue) uz). case: (oltNge (all_der_p5 oj luz) h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)