proposition: Lemma CReal_mult_assoc : forall x y z : CReal, (x * y) * z == x * (y * z).
proof: Proof. intros x y z; apply CRealEq_diff; intros n. unfold CReal_mult, CReal_mult_seq, CReal_mult_scale. do 4 rewrite CReal_red_seq. do 2 rewrite CReal_red_scale. do 6 simplify_seq_idx. replace (n - scale z - scale y)%Z with (n - scale y - scale z)%Z by ring. replace (n - scale z - scale x)%Z with (n - scale x - scale z)%Z by ring. simplify_Qabs. assert (forall a1 a2 b c1 c2 : Q, a1*b*c1+(-1)*b*a2*c2==(a1*c1-a2*c2)*b)%Q as H by (intros; ring). rewrite H; clear H. remember (seq x (n - scale y - scale z - 1) - seq x (n - scale y - scale z - 2))%Q as dx eqn:Heqdx. remember (seq z (n - scale x - scale y - 1) - seq z (n - scale x - scale y - 2))%Q as dz eqn:Heqdz. setoid_replace (seq x (n - scale y - scale z - 1)) with (seq x (n - scale y - scale z - 2) + dx)%Q by (rewrite Heqdx; ring). setoid_replace (seq z (n - scale x - scale y - 1)) with (seq z (n - scale x - scale y - 2) + dz)%Q by (rewrite Heqdz; ring). match goal with |- (Qabs (?a * _) <= _)%Q => ring_simplify a end. pose proof bound x (n - scale y - scale z - 2)%Z as Hbndx. pose proof bound z (n - scale x - scale y - 2)%Z as Hbndz. pose proof bound y (n - scale x - scale z - 2)%Z as Hbndy. pose proof cauchy x (n - scale y - scale z - 1)%Z (n - scale y - scale z - 1)%Z (n - scale y - scale z - 2)%Z ltac:(lia) ltac:(lia) as Hbnddx; rewrite <- Heqdx in Hbnddx; clear Heqdx. pose proof cauchy z (n - scale x - scale y - 1)%Z (n - scale x - scale y - 1)%Z (n - scale x - scale y - 2)%Z ltac:(lia) ltac:(lia) as Hbnddz; rewrite <- Heqdz in Hbnddz; clear Heqdz. rewrite Qabs_Qmult. replace n with ((n - scale y) + scale y)%Z at 4 by lia. rewrite Qpower_plus by lra. rewrite Qmult_assoc. apply Qmult_le_compat_nonneg. 2: (split; [apply Qabs_nonneg | lra]). split; [apply Qabs_nonneg|]. apply (Qle_trans _ _ _ (Qabs_triangle _ _)). setoid_replace (2 * 2 ^ (n - scale y))%Q with (2 ^ (n - scale y) + 2 ^ (n - scale y))%Q by ring. apply Qplus_le_compat. - rewrite Qabs_Qmult. replace (n - scale y)%Z with (scale x + (n - scale x - scale y))%Z at 2 by lia. rewrite Qpower_plus by lra. apply Qmult_le_compat_nonneg. + (split; [apply Qabs_nonneg | lra]). + split; [apply Qabs_nonneg|]. apply (Weaken_Qle_QpowerRemSubExp _ _ 1 ltac:(lia)), Qlt_le_weak, Hbnddz. - rewrite Qabs_Qmult. replace (n - scale y)%Z with (scale z + (n - scale y - scale z))%Z by lia. rewrite Qpower_plus by lra. apply Qmult_le_compat_nonneg. + split; [apply Qabs_nonneg|]. rewrite <- Qabs_opp; simplify_Qabs; lra. + split; [apply Qabs_nonneg|]. apply (Weaken_Qle_QpowerRemSubExp _ _ 1 ltac:(lia)), Qlt_le_weak, Hbnddx. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra