Solve slowdown in derive

[CohenCyril]

TODO (alternatives):

• Lock the definition of diffusing a module type :

  analysis/derive.v

  Lines 46 to 48 in 99d2078

  	Definition diff (F : filter_on V) (_ : phantom (set (set V)) F) (f : V -> W) :=
  	(get (fun (df : {linear V -> W}) => continuous df /\ forall x,
  	f x = f (lim F) + df (x - lim F) +o_(x \near F) (x - lim F))).

• Use canonical structures instead of typeclasses for automatic derive