proposition: Lemma idO (F : filter_on T) (e : T -> W) : e =O_F e.
proof: Proof. by apply/eqO_exP; exists 1 => //; apply: filterE=> x; rewrite mul1r. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule