The proof of near_derive can be simplified

[affeldt-aist]

analysis/theories/derive.v

Lines 1869 to 1886 in 762e08b

	Let near_derive :
	{near 0^', (fun h => h^-1 *: (f (h *: v + a) - f a)) =1
	(fun h => h^-1 *: (g (h *: v + a) - g a))}.
	Proof.
	near do congr (_ *: _).
	move: afg; rewrite {1}/prop_near1/= nbhsE/= => -[B [oB Ba] /[dup] Bfg Bfg'].
	have [e /= e0 eB] := open_subball oB Ba.
	have vv0 : 0 < `|2 *: v| by rewrite normrZ mulr_gt0 ?normr_gt0.
	near=> x.
	have x0 : 0 < `|x| by rewrite normr_gt0//; near: x; exact: nbhs_dnbhs_neq.
	congr (_ - _); last exact: Bfg'.
	apply: Bfg; apply: (eB (`|x| * `|2 *: v|)).
	- rewrite /ball_/= sub0r normrN normrM !normr_id -ltr_pdivlMr//.
	by near: x; apply: dnbhs0_lt; rewrite divr_gt0.
	- by rewrite mulr_gt0.
	- rewrite -ball_normE/= opprD addrCA subrr addr0 normrN normrZ ltr_pM2l//.
	by rewrite normrZ ltr_pMl ?normr_gt0// gtr0_norm ?ltr1n.
	Unshelve. all: by end_near. Qed.

see this comment @CohenCyril