proposition: Lemma CV_extensionality : forall Un Un', (forall n, Un n = Un' n) -> forall l, Un_cv Un l -> Un_cv Un' l.
proof: Proof. intros Un Un' H_ext l. unfold Un_cv; intros H_lim eps H_eps. destruct (H_lim eps H_eps) as [N H_N]. exists N. intros n H_n'. rewrite <- (H_ext n); apply H_N; trivial. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)