proposition: Lemma all_der_p12_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) -> (forall x i, x <o z -> ordinalp i -> g x i = x).
proof: Proof. move => ha hb oz fp x i xi oi0;move:x xi. move: i oi0; apply: least_ordinal2 => i oi etc x xz. have ox:= proj31_1 xz. case (ozero_dichot oi) => iz. by rewrite iz /g (all_der_p2 ha hb ox) (fp _ xz). have hc: forall x, x <o z -> exists2 t, t <=o x & x = g t i. move => u uz. have ou:= proj31_1 uz. have hh: forall k, k<o i -> g u k = u by move => k ki; move: (etc _ ki _ uz). move:(all_der_p8 ha hb ou iz hh) => [t ot]; rewrite -/g => eq1. move: (proj1 (all_der_p6 ha hb oi)) => hc. by move:(osi_gex hc ot); rewrite -/g - eq1 => tu; exists t. apply: (least_ordinal2(p:= fun x => x<o z -> g x i = x)) ox (xz) => x0 ox0 etc2. move => le2. move: (hc _ le2) => [t ta eq1]. case (equal_or_not t x0) => eq2; first by rewrite - eq2 - eq1. by move: (etc2 _ (conj ta eq2) (ole_ltT ta le2)) => eq3;rewrite eq1 eq3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)