proposition: Lemma CReal_mult_bound : forall (x y : CReal), QBound (CReal_mult_seq x y) (CReal_mult_scale x y).
proof: Proof. intros x y k. unfold CReal_mult_seq, CReal_mult_scale. pose proof (bound x (k - scale y - 1)%Z) as Hxbnd. pose proof (bound y (k - scale x - 1)%Z) as Hybnd. pose proof Qabs_nonneg (seq x (k - scale y - 1)) as Habsx. pose proof Qabs_nonneg (seq y (k - scale x - 1)) as Habsy. rewrite Qabs_Qmult; rewrite Qpower_plus by lra. apply Qmult_lt_compat_nonneg; lra. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra