proposition: Lemma closely_norm_le_closely : filter_le closely_norm closely.
proof: Proof. intros P [eps H]. exists eps. intros u v Buv. apply H. now apply norm_compat1. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub