proposition: Lemma eqTheta_trans (F : filter_on T) (f g h : T -> V) : f =Theta_F g -> g =Theta_F h -> f =Theta_F h.
proof: Proof. rewrite !eqThetaE !bigThetaE -!eqOmegaE => -[fg gf] [gh hg]; split. by rewrite fg (bigO_bigO_eqO _ _ _ gh). exact: (eqOmega_trans gf hg). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule