proposition: Lemma all_der_p7 x i j: ordinalp x -> i <o j -> g (g x j) i = g x j.
proof: Proof. move => ox ij. move: (ij) => [[oi oj _] _]. move: (all_der_bound_prop ox oj bf). set C:= union _; set E:= cnext C. move => [sa sb sc sd se]. rewrite sd in sb sc se. have ie: inc i E. move: (proj1 (CS_cnext (proj1 sa))) => ose. move/(oltP ose): sc => /(olt_ltT ij) lt1. by apply/(oltP ose). set ge:= all_der_aux f E. set y := (g x j). have ye: inc y E by rewrite - sd; apply:all_der_p3. have v1:= (all_der_p1 sa ye ie se). have v2:= (all_der_p1 sa sb sc se). have jnz: j <> \0o by move => h; move: ij; rewrite h; exact:olt0. move: (all_der_bound_prop2 ox oj); rewrite sd => sf. move:(many_der_ex sa sf); rewrite -/E. set ff:=(many_der (Lf f E E) E). move => [ua ub uc ud [_ _ ug uh]]. have h:= (ud _ sc jnz). have v3: y = Vf (Vf ff j) x by rewrite /y v2. move: (ug _ sc) => [[pa pb pc] _ _]. have ij': inc i j by apply/oltP => //. have: inc y (Imf (Vf ff j)). rewrite v3; apply/(Imf_P pa); exists x => //; ue. rewrite (uh j sc jnz) v1 => h1. by move: (setIf_hi h1 ij') => /Zo_hi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)