proposition: Lemma bigTheta_refl_subproof F (g : T -> V) : Filter F -> bigTheta_def F g g.
proof: Proof. by move=> FF; exists 1 => /=; rewrite ?ltr01 //; near=> x; by rewrite mul1r. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule