proposition: Lemma equivoRL (W' : normedModType K) F (f g : T -> V) (h : T -> W') : f ~_F g -> [o_F g of h] =o_F f.
proof: Proof. move=> ->; apply/eqoP; move=> _/posnumP[eps]; near=> x. rewrite -ler_pdivrMl // -[X in g + X]opprK oppo. rewrite (le_trans _ (ler_dist_dist _ _)) //. rewrite [leRHS]ger0_norm ?lerBrDr ?add0r; last first. by rewrite -[leRHS]mul1r; near: x; apply: littleoP. rewrite [leRHS]splitr [_ / 2]mulrC. by rewrite lerD ?ler_pdivrMl ?mulrA //; near: x; apply: littleoP. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule