proposition: Lemma extension_cont_is_derive (f g : R -> V) (a : R) (l : V) : is_derive f a l -> is_derive g a l -> f a = g a -> is_derive (extension_cont f g a) a l.
proof: Proof. case => _ Cf [_ Cg] Heq. split. by apply is_linear_scal_l. move => x Hx eps. move: (Cf x Hx eps) => {} Cf. move: (Cg x Hx eps) => {} Cg. generalize (is_filter_lim_locally_unique _ _ Hx) => {} Hx. rewrite -Hx {x Hx} in Cf, Cg |- *. generalize (filter_and _ _ Cf Cg). apply filter_imp => {Cf Cg} x [Cf Cg]. rewrite /extension_cont. case: Rle_dec => Hx ; case: Rle_dec (Rle_refl a) => //= _ _. by rewrite Heq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv