proposition: Lemma is_domin_le {F G} (f : T -> U) (g : T -> V) : is_domin F f g -> filter_le G F -> is_domin G f g.
proof: Proof. intros. intros eps. by apply H0. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy