proposition: Lemma bigTheta {W} (F : filter_on T) (g : T -> W) (f : {Theta_F g}) : bigTheta_spec F g f.
proof: Proof. have [[_ _] /andP[/posnumP[k] /posnumP[k']]] := bigThetaP f. by move=> /near_andP[]; exists k k'. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule