proposition: Lemma CReal_opp_cauchy : forall (x : CReal), QCauchySeq (CReal_opp_seq x).
proof: Proof. intros x n p q Hp Hq; unfold CReal_opp_seq. pose proof ((cauchy x) n p q ltac:(lia) ltac:(lia)) as Hxbnd. rewrite Qabs_Qlt_condition in Hxbnd |- *. lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra