fact: Definition bigOmega_refl (F : filter_on T) g := BigOmega (asboolT (@bigOmega_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