proposition: Lemma eqOmega_trans (F : filter_on T) (f g h : T -> V) : f =Omega_F(g) -> g =Omega_F(h) -> f =Omega_F(h).
proof: Proof. rewrite !eqOmegaE !eqOmegaO => fg gh; exact: (eqO_trans gh fg). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule