proposition: Lemma CV_const: forall const, Un_cv (fun i : nat => const) const.
proof: Proof. intros const eps H_eps; exists 0%nat; intros n _; rewrite Rfunctions.R_dist_eq; trivial. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)