proposition: Lemma addO (F : filter_on T) (f g: T -> V) e : [O_F e of f] + [O_F e of g] =O_F e.
proof: Proof. by rewrite [RHS]bigOE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule