proposition: Lemma ex_strict_dom_bound {T : Type} {K : numFieldType} {V W : pseudoMetricNormedZmodType K} (h : T -> V) (f : T -> W) (F : set_system T) {PF : ProperFilter F} : (\forall x \near F, h x != 0) -> (\forall M \near +oo, dominated_by h M f F) <-> exists M, strictly_dominated_by h M f F.
proof: Proof. move=> hN0; rewrite ex_dom_bound /dominated_by /strictly_dominated_by. split => -[] M FM; last by exists M; apply: filterS FM => x /ltW. exists (M + 1); apply: filterS2 hN0 FM => x hN0 /le_lt_trans/= ->//. by rewrite ltr_pM2r ?normr_gt0// ltrDl. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule