wip

Author: affeldt-aist

tilt.v

@@ -234,11 +234,17 @@ rewrite [X in (X @ _)%classic](_ : _ = scalar_mx \o (fun h =>
     (h^-1 *: ((f (h *: 'e_i + a)) - (f a))))); last first.
   apply/funext => h.
   rewrite /=.
-  admit.
+  rewrite -scale_scalar_mx.
+  congr (_ *: _).
+  rewrite raddf/=.
+  f_equal.
+  by rewrite raddfN.
 apply/cvg_lim => //=.
 apply: (@cvg_comp _ _ _ _ scalar_mx _
 (nbhs (lim ((h^-1 *: (f (h *: 'e_i + a) - f a)) @[h --> 0^']))%classic)).
   admit.
+
+
 Admitted.
 
 Lemma partialE {R : realType} n (f : 'rV[R]_n.+1 -> R)  (a : 'rV[R]_n.+1)