fact: Definition bigTheta_refl (F : filter_on T) g := BigTheta (asboolT (@bigTheta_refl_subproof F g _)).
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule