proposition: Lemma equivOLR F (f g : T -> V) : f ~_F g -> f =O_F g.
proof: Proof. by move=> ->; apply: eqOE; rewrite {1}[g](idO F) addrC addfO. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule