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