proposition: Fact dinv (x : R) : x != 0 -> continuous (fun h : R => - x ^- 2 *: h) /\ (fun x => x^-1)%R \o shift x = cst (x^-1)%R + (fun h : R => - x ^- 2 *: h) +o_ (0 : R) id.
proof: Proof. move=> xn0; suff: continuous (fun h : R => - (1 / x) ^+ 2 *: h) /\ (fun x => 1 / x ) \o shift x = cst (1 / x) + (fun h : R => - (1 / x) ^+ 2 *: h) +o_ (0 : R) id. rewrite !mul1r !GRing.exprVn. rewrite (_ : (fun x => x^-1) = (fun x => 1 / x ))//. by rewrite funeqE => y; rewrite mul1r. split; first by move=> ?; apply: continuousZr. apply/eqaddoP => _ /posnumP[e]; near=> h. rewrite -[(_ + _ : R -> R) h]/(_ + _) -[(- _ : R -> R) h]/(- _) /=. rewrite opprD scaleNr opprK /cst /=. rewrite -[- _]mulr1 -[X in - _ * X](mulfVK xn0) mulrA mulNr -expr2 mulNr. rewrite [- _ + _]addrC -mulrBr. rewrite -[X in X + _]mulr1 -[X in 1 / _ * X](@mulfVK _ (x ^+ 2)); last first. by rewrite sqrf_eq0. rewrite mulrA mulf_div mulr1. have hDx_neq0 : h + x != 0. near: h; rewrite !nbhs_simpl; apply/nbhs_normP. exists `|x|; first by rewrite /= normr_gt0. move=> h /=; rewrite /= distrC subr0 -subr_gt0 => lthx. rewrite -(normr_gt0 (h + x)) addrC -[h]opprK. apply: lt_le_trans (ler_dist_dist _ _). by rewrite ger0_norm normrN //; apply: ltW. rewrite addrC -[X in X * _]mulr1 -{2}[1](@mulfVK _ (h + x)) //. rewrite mulrA expr_div_n expr1n mulf_div mulr1 [_ ^+ 2 * _]mulrC -mulrA. rewrite -mulrDr mulrBr [1 / _ * _]mulrC normrM. rewrite mulrDl mulrDl opprD addrACA addrA [x * _]mulrC expr2 2!subrK. rewrite div1r normfV [X in _ / X]normrM invfM [X in _ * X]mulrC. rewrite mulrA mulrAC ler_pdivrMr ?normr_gt0 ?mulf_neq0 //. rewrite mulrAC ler_pdivrMr ?normr_gt0 //. have : `|h * h| <= `|x / 2| * (e%:num * `|x * x| * `|h|). rewrite !mulrA; near: h; exists (`|x / 2| * e%:num * `|x * x|). by rewrite /= !pmulr_rgt0 // normr_gt0 mulf_neq0. by move=> h /ltW; rewrite distrC subr0 [`|h * _|]normrM => /ler_pM; apply. move=> /le_trans -> //; rewrite [leLHS]mulrC ler_pM ?mulr_ge0 //. near: h; exists (`|x| / 2); first by rewrite /= divr_gt0 ?normr_gt0. move=> h; rewrite /= distrC subr0 => lthhx; rewrite addrC -[h]opprK. apply: le_trans (@ler_dist_dist _ R _ _). rewrite normrN [leRHS]ger0_norm; last first. rewrite subr_ge0; apply: ltW; apply: lt_le_trans lthhx _. by rewrite ler_pdivrMr // -{1}(mulr1 `|x|) ler_pM // ler1n. rewrite lerBrDr -lerBrDl (splitr `|x|). by rewrite normrM normfV (@ger0_norm _ 2) // -addrA subrr addr0; apply: ltW. Unshelve. all: by end_near. 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