proposition: Lemma seq_cv_proper : forall (un : nat -> CReal) (a b : CReal), seq_cv un a -> a == b -> seq_cv un b.
proof: Proof. intros. intro p. specialize (H p) as [n H]. exists n. intros. rewrite <- H0. apply H, H1. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra