proposition: Lemma eqaddOo_trans (F : filter_on T) (f g h : T -> V) fg gh (e : T -> W): f = g + [O_ F e of fg] -> g = h + [o_F e of gh] -> f = h +O_F e.
proof: Proof. by move=> -> ->; rewrite -addrA addfO. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule