proposition: Lemma domin_antisym {T} {K : AbsRing} {V : NormedModule K} : forall {F : (T -> Prop) -> Prop} {FF : ProperFilter F} (f : T -> V), F (fun x => norm (f x) <> 0) -> ~ is_domin F f f.
proof: Proof. intros F FF f Hf H. move: (H (pos_div_2 (mkposreal _ Rlt_0_1))) => {H} /= H. apply filter_const. generalize (filter_and _ _ H Hf) => {H Hf}. apply filter_imp. intros x [H1 H2]. generalize (norm_ge_0 (f x)). lra. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy