Remove this lemma about derivative and replace.

[CohenCyril]

analysis/derive.v

Line 135 in e2d3d4c

derivative1 f a = lim ((fun x => ('d_a f x) / x) @ (0 : R^o)).

'd_a f x / x although valid is a non canonical way for getting the coefficient of a linear map (no need to take a limit by the way, it is supposed to be constant). The canonical way is to first take the Jacobian (using lin1_mx) and in dimension 1 (since R^o is), just take the only coefficient: jacobian f 0 0.

derivative1 f a = 'J_a f 0 0

[affeldt-aist]

The desired lemma has been renamed derivemxE in the meantime and depends on deriveE that now has a tentative proof.