proposition: Lemma locally_norm_le_locally : forall x, filter_le (locally_norm x) (locally x).
proof: Proof. intros x P [eps H]. exists eps. intros y By. apply H. now apply norm_compat1. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub