proposition: Lemma all_der_p13_bis f b (g:= all_der f b) z: normal_ofs f ->all_der_bound f b -> ordinalp z -> (forall x, x <o z -> f x = x) -> f z <> z -> normal_ofs (g z).
proof: Proof. move => ha hb oz hc fzz. move: (all_der_p12_bis ha hb oz hc) => hd. set fs := (fun t => f (z +o t) -o z). move: (normal_shift ha oz);rewrite -/fs => ha'. pose bs x i := b (z +o x) i. have hb': all_der_bound fs bs. move => x i ox oi; move:(hb _ _ (OS_sum2 oz ox) oi);rewrite /bs. move => [pa pb pc pd]; move: (pc) => [C ic eq]. have oE := (proj1 (CS_cnext (proj1 ic))). rewrite eq in pa;move/(oltP oE): pa => pa'. have zE: inc z (b (z +o x) i). by move: (ole_ltT(osum_Mle0 oz ox) pa')=> pa''; rewrite eq; apply/(oltP oE). have pe: inc x (b (z +o x) i). by move: (ole_ltT(osum_M0le oz ox) pa')=> pa''; rewrite eq; apply/(oltP oE). split => // t tE. have: inc (z +o t) (b (z+o x) i). move: zE tE; move: (cnext_sum ic); rewrite -eq; apply. move/pd; rewrite eq; move/(oltP oE) => za; apply /(oltP oE). exact: (ole_ltT (odiff_Mle oz (proj31_1 za)) za). have zfz: z <o f z. split; fprops; exact: (osi_gex (proj1 ha) oz). have fsz: fs \0o <> \0o. by rewrite /fs (osum0r oz) => h; move: (odiff_pos zfz) => []; rewrite h. move: (all_der_p13 ha' hb' fsz) => he. set gs:= (all_der fs bs). have ns:= (osum_normal oz). suff: forall i, ordinalp i -> forall x, ordinalp x -> z +o (gs x i) = g (z +o x) i. move => h. have n1: forall i, ordinalp i -> g z i = z +o (gs \0o i). by move => i oi; move: (h i oi \0o OS0); rewrite (osum0r oz). move: (normal_ofs_compose ns he). by apply:normal_ofs_from_exten => t ot /=; rewrite - n1. apply: least_ordinal2 => i oi etc. have pa: forall f x, normal_ofs f -> ordinalp x -> (ordinalp (f (z +o x) -o z) /\ z +o (f (z +o x) -o z) = f (z +o x)). move => h x [sih _] ox; move:(osi_gex sih (OS_sum2 oz ox))=> xh. by move: (odiff_pr (oleT (osum_Mle0 oz ox) xh)) => []. move => x ox. have na: normal_ofs (fun x => z +o gs x i). exact: (normal_ofs_compose ns (all_der_p6 ha' hb' oi)). have nb: normal_ofs (fun x => g (z +o x) i). exact: (normal_ofs_compose (all_der_p6 ha hb oi) ns). case (ozero_dichot oi) => iz. have ozx: ordinalp (z +o x) by fprops. rewrite iz /g /gs (all_der_p2 ha hb ozx) (all_der_p2 ha' hb' ox). apply: (proj2 (pa _ _ ha ox)). have ee: forall y j, j <o i -> ordinalp y -> z +o gs y j = g (z +o y) j. by move => y j ji oy; move:(etc _ ji _ oy). move: x ox. apply:(sincr_ofs_exten (proj1 na) (proj1 nb)) => x ox. move: (ofs_sincr (proj1 na) ox) => o1. have ot: (ordinalp (gs x i)) by apply: (OS_all_der ha' hb' ox oi). have h: forall j, j <o i -> g (z +o gs x i) j = z +o gs x i. move => j ji. by rewrite - (ee _ _ ji ot) /gs (all_der_p7 ha' hb' ox ji). move: (all_der_p8 ha hb o1 iz h) => [y y1 y2]; rewrite y2 -/g. case: (oleT_el oz y1) => eq1. by move: (odiff_pr eq1) => [sa sb]; exists (y -o z) => //; rewrite - sb. by move: y2 (osum_Mle0 oz ot);rewrite (hd _ _ eq1 oi) => -> /(oltNge eq1). set u :=(g (z +o x) i -o z). move: (pa _ x (all_der_p6 ha hb oi) ox) => []; rewrite -/g -/u => [ou uv]. have h: forall j, j <o i -> all_der fs bs u j = u. move => j ji. have ogu:= (OS_all_der ha' hb' ou (proj31_1 ji)). apply: (osum2_simpl ogu ou oz); rewrite ee // uv. exact:(all_der_p7 ha hb (OS_sum2 oz ox) ji). rewrite - uv. by move: (all_der_p8 ha' hb' ou iz h) => [y oy ->]; exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)