proposition: Lemma all_der_p8 y j: ordinalp y -> \0o <o j -> (forall i, i <o j -> g y i = y) -> (exists2 x, ordinalp x & y = g x j).
proof: Proof. move => oy jp h. have oj:=proj32_1 jp. have jnz:= nesym (proj2 jp). move: (all_der_bound_prop oy oj bf). set C:= union _; set E:= cnext C. move => [sa sb sc sd se]. move: (all_der_bound_prop2 oy oj); rewrite sd => sf. rewrite sd in sb sc se. move:(many_der_ex sa sf); rewrite -/E. set ff:=(many_der (Lf f E E) E). move => [ua ub uc ud [_ _ ug uh]]. move: (proj1 (CS_cnext (proj1 sa))) => oe. suff:inc y (Imf (Vf ff j)). move: (ug _ sc) => [[pa pb pc] _ _ ]. move /(Imf_P pa); rewrite pb; move => [u ue uv]; exists u. exact: (Os_ordinal oe ue). by rewrite uv (all_der_p1 sa ue sc). rewrite (uh j sc jnz). have nej: nonempty j by exists \0o;move: (olt_i jp). apply /setIf_P => // i ij. have ij1: i <o j by apply/(oltP oj). have iE: inc i E. by move/(oltP oe): sc => /(olt_ltT ij1) /olt_i. move: (ug _ iE) => [[pa pb pc] _ _ ]. apply /Zo_P; rewrite pb; split => //. by move:(h _ ij1);rewrite (all_der_p1 sa sb iE se). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)