proposition: Lemma all_der_p1 x i C (E:= cnext C): infinite_c C -> inc x E -> inc i E -> (forall t, inc t E -> inc (f t) E) -> g x i = all_der_aux f E x i.
proof: Proof. move => pc xe ie esf. move: (proj1 (CS_cnext (proj1 pc))) => oe. move: (Os_ordinal oe xe) (Os_ordinal oe ie) => ox oi. have n1:=(all_der_bound_prop2 ox oi). have n2:=(normal_ofs_restriction pc nf esf). have aux: forall C C', C <=c C' -> sub (cnext C) (cnext C'). move => C1 C2 cc; move: (cc) => [c1 c2 _]. move => t /(cnextP c1) [sa sb]; apply/(cnextP c2). by move:(cleT sb cc). move:(all_der_bound_prop ox oi bf). set C1 := union _; move => [sa sb sc sd se]. rewrite {3 4} sd in n1. case: (cleT_ee (proj1 pc) (proj1 sa)) => cc. have see: sub E (b x i) by rewrite sd;apply: aux. have ag: agrees_on E (Lf f E E) (Lf f (b x i) (b x i)). by hnf; aw; split => // => t te /=; rewrite !LfV//; apply: see. move: (many_der_unique cc pc sa ag n2 n1 ie) => [_ _ h]. by symmetry; move: (h _ xe); rewrite - sd. have see: sub (b x i) E by rewrite sd;apply: aux. have ag: agrees_on (b x i) (Lf f (b x i) (b x i)) (Lf f E E). by hnf; aw; split => // => t te /=; rewrite !LfV//; apply: see. rewrite {1} sd in ag; rewrite sd in sb sc. move: (many_der_unique cc sa pc ag n1 n2 sc)=> [_ _ h]. by move: (h _ sb); rewrite - sd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)