proposition: Fact der_mult f g (x v : V) : derivable f x v -> derivable g x v -> (fun h => h^-1 *: (((f * g) \o shift x) (h *: v) - (f * g) x)) @ (0 : R)^' --> f x *: 'D_v g x + g x *: 'D_v f x.
proof: Proof. move=> df dg. evar (fg : R -> R); rewrite [X in X @ _](_ : _ = fg) /=; last first. rewrite funeqE => h. have -> : (f * g) (h *: v + x) - (f * g) x = f (h *: v + x) *: (g (h *: v + x) - g x) + g x *: (f (h *: v + x) - f x). by rewrite !scalerBr -addrA ![g x *: _]mulrC addKr. rewrite scalerDr scalerA mulrC -scalerA. by rewrite [_ *: (g x *: _)]scalerA mulrC -scalerA /fg. apply: cvgD; last exact: cvgZr df. apply: cvg_comp2 (@mul_continuous _ (_, _)) => /=; last exact: dg. suff : {for 0, continuous (fun h : R => f(h *: v + x))}. by move=> /continuous_withinNx; rewrite scale0r add0r. exact/differentiable_continuous/derivable1_diffP/(derivable1P _ _ _).1. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms