proposition: Lemma CReal_plus_cauchy : forall (x y : CReal), QCauchySeq (CReal_plus_seq x y).
proof: Proof. intros x y n p q Hp Hq. unfold CReal_plus_seq. pose proof ((cauchy x) (n-1)%Z (p-1)%Z (q-1)%Z ltac:(lia) ltac:(lia)) as Hxbnd. pose proof ((cauchy y) (n-1)%Z (p-1)%Z (q-1)%Z ltac:(lia) ltac:(lia)) as Hybnd. do 2 rewrite Qred_correct. rewrite Qabs_Qlt_condition in Hxbnd, Hybnd |- *. rewrite Qpower_minus_pos in Hxbnd, Hybnd. lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra