proposition: Lemma all_der_p6 i: ordinalp i -> normal_ofs (g ^~i).
proof: Proof. move => oi. split; first by move => x y xy;apply:all_der_p5. move => x lx. move: (lx) => [ox _ _]. have osx: forall y, inc y x -> y <o x by move => y /(oltP ox). pose g1 y := all_der_aux f (b x i) y i. have -> : g x i = g1 x by []. have -> : fun_image x (g^~ i) = fun_image x g1. have h: forall z, inc z x -> g z i = g1 z. move => z zx. have zx': z <o x by apply/(oltP ox). by move: (all_der_p4 oi zx') => [_ -> _]. by set_extens t; move =>/funI_P [z zx ->]; apply/funI_P; ex_tac; rewrite h. have [sa sb sc sd se] := (all_der_bound_prop ox oi bf). move: (all_der_bound_prop2 ox oi); rewrite sd => sf. move:(many_der_ex sa sf) => [_ _ _ _ [_ _ ug _]]. rewrite - sd in ug. move: (ug _ sc); set g2 := (Vf _ _). have <-: Vf g2 x = g1 x by []. move => [[ fg2 sg2 _] hb hc]; rewrite (hc _ sb lx); congr union. have sgx: sub x (source g2). rewrite sg2;apply:ordinal_transitive => //; rewrite sd. exact: (proj1 (CS_cnext (proj1 sa))). set_extens t. move/(Vf_image_P fg2 sgx) => [u ut ->]; apply/funI_P; ex_tac. move /funI_P=> [u ut ->]; apply /(Vf_image_P fg2 sgx); ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)