proposition: Lemma CReal_mult_plus_distr_l : forall r1 r2 r3 : CReal, r1 * (r2 + r3) == (r1 * r2) + (r1 * r3).
proof: Proof. intros x y z; apply CRealEq_diff; intros n. unfold CReal_mult, CReal_mult_seq, CReal_mult_scale, CReal_plus, CReal_plus_seq, CReal_plus_scale. do 5 rewrite CReal_red_seq. do 1 rewrite CReal_red_scale. do 2 rewrite Qred_correct. do 5 simplify_seq_idx. simplify_Qabs. assert (forall y' z': CReal, Qabs ( seq x (n - Z.max (scale y') (scale z') - 2) * seq y' (n - scale x - 2) - seq x (n - scale y' - 2) * seq y' (n - scale x - 2)) <= 2 ^ n )%Q as Hdiffbnd. { intros y' z'. assert (forall a b c : Q, a*c-b*c==(a-b)*c)%Q as H by (intros; ring). rewrite H; clear H. pose proof cauchy x (n - (scale y') - 2)%Z (n - Z.max (scale y') (scale z') - 2)%Z (n - scale y' - 2)%Z ltac:(lia) ltac:(lia) as Hxbnd. pose proof bound y' (n - scale x - 2)%Z as Hybnd. replace n with ((n - scale y' - 2) + scale y' + 2)%Z at 4 by lia. apply Weaken_Qle_QpowerAddExp. { lia. } rewrite Qpower_plus, Qabs_Qmult by lra. apply Qmult_le_compat_nonneg; (split; [apply Qabs_nonneg | lra]). } pose proof Hdiffbnd y z as Hyz. pose proof Hdiffbnd z y as Hzy; clear Hdiffbnd. pose proof Qplus_le_compat _ _ _ _ Hyz Hzy as Hcomb; clear Hyz Hzy. apply (Qle_trans _ _ _ (Qabs_triangle _ _)) in Hcomb. rewrite (Z.max_comm (scale z) (scale y)) in Hcomb . rewrite Qabs_Qle_condition in Hcomb |- *. lra. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra