proposition: Lemma closely_le_closely_norm : filter_le closely closely_norm.
proof: Proof. intros P [eps H]. assert (He : 0 < / norm_factor * eps). apply Rmult_lt_0_compat. apply Rinv_0_lt_compat. apply norm_factor_gt_0. apply cond_pos. exists (mkposreal _ He). intros u v Buv. apply H. unfold ball_norm. rewrite -(Rmult_1_l eps) -(Rinv_r norm_factor). rewrite Rmult_assoc. apply norm_compat2 with (1 := Buv). apply Rgt_not_eq. apply norm_factor_gt_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub