proposition: Lemma CReal_plus_bound : forall (x y : CReal), QBound (CReal_plus_seq x y) (CReal_plus_scale x y).
proof: Proof. intros x y k. unfold CReal_plus_seq, CReal_plus_scale. pose proof (bound x (k-1)%Z) as Hxbnd. pose proof (bound y (k-1)%Z) as Hybnd. rewrite Qpower_plus by lra. pose proof Qpower_le_compat_l 2 (scale x) (Z.max (scale x) (scale y)) ltac:(lia) ltac:(lra) as Hxmax. pose proof Qpower_le_compat_l 2 (scale y) (Z.max (scale x) (scale y)) ltac:(lia) ltac:(lra) as Hymax. rewrite Qabs_Qlt_condition in Hxbnd, Hybnd |- *. rewrite Qred_correct. lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra