proposition: Lemma oppox (F : filter_on T) (f : T -> V) e x : - [o_F e of f] x = [o_F e of - [o_F e of f]] x.
proof: Proof. by move: x; rewrite -/(- _ =1 _) {1}oppo. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule