proposition: Lemma CReal_abs_cauchy: forall (x : CReal), QCauchySeq (CReal_abs_seq x).
proof: Proof. intros x n p q Hp Hq. pose proof (cauchy x n p q Hp Hq) as Hxbnd. apply (Qle_lt_trans _ (Qabs (seq x p - seq x q))). 2: exact Hxbnd. apply Qabs_Qle_condition. split. 2: apply Qabs_triangle_reverse. apply (Qplus_le_r _ _ (Qabs (seq x q))). rewrite <- Qabs_opp. apply (Qle_trans _ _ _ (Qabs_triangle_reverse _ _)). ring_simplify. unfold CReal_abs_seq. simplify_Qabs; setoid_rewrite Qopp_mult_mone. do 2 rewrite Qabs_opp. lra. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra