proposition: Lemma CReal_mult_cauchy: forall (x y : CReal), QCauchySeq (CReal_mult_seq x y).
proof: Proof. intros x y n p q Hp Hq. unfold CReal_mult_seq. assert(forall xp xq yp yq : Q, xp * yp - xq * yq == (xp - xq) * yp + xq * (yp - yq))%Q as H by (intros; ring). rewrite H; clear H. apply (Qle_lt_trans _ _ _ (Qabs_triangle _ _)). do 2 rewrite Qabs_Qmult. replace n with ((n-1)+1)%Z by ring. rewrite Qpower_plus by lra. setoid_replace (2 ^ (n - 1) * 2 ^1)%Q with (2 ^ (n - 1) + 2 ^ (n - 1))%Q by ring. apply Qplus_lt_le_compat. - apply (Qle_lt_trans _ ((2 ^ (n - scale y - 1)) * Qabs (seq y (p - scale x - 1)))). + apply Qmult_le_compat_r. 2: apply Qabs_nonneg. apply Qlt_le_weak. apply (cauchy x); lia. + apply (Qmult_lt_l _ _ (2 ^ -(n - scale y - 1))%Q). { apply Qpower_0_lt; lra. } rewrite Qmult_assoc, <- Qpower_plus by lra. rewrite <- Qpower_plus by lra. simplify_Qpower_exponent; rewrite Qpower_0_r, Qmult_1_l. simplify_Qpower_exponent. apply (bound y). - apply Qlt_le_weak. apply (Qle_lt_trans _ ((2 ^ (n - scale x - 1)) * Qabs (seq x (q - scale y - 1)))). + rewrite Qmult_comm; apply Qmult_le_compat_r. 2: apply Qabs_nonneg. apply Qlt_le_weak; apply (cauchy y); lia. + apply (Qmult_lt_l _ _ (2 ^ -(n - scale x - 1))%Q). { apply Qpower_0_lt; lra. } rewrite Qmult_assoc, <- Qpower_plus by lra. rewrite <- Qpower_plus by lra. simplify_Qpower_exponent; rewrite Qpower_0_r, Qmult_1_l. simplify_Qpower_exponent. apply (bound x). Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra