proposition: Lemma CReal_plus_assoc : forall (x y z : CReal), (x + y) + z == x + (y + z).
proof: Proof. intros x y z; apply CRealEq_diff; intro n. unfold CReal_plus, CReal_plus_seq. do 4 rewrite CReal_red_seq. do 4 rewrite Qred_correct. ring_simplify (n-1-1)%Z. pose proof ((cauchy x) (n-1)%Z (n-2)%Z (n-1)%Z ltac:(lia) ltac:(lia)) as Hxbnd. specialize ((cauchy z) (n-1)%Z (n-2)%Z (n-1)%Z ltac:(lia) ltac:(lia)) as Hzbnd. apply Qlt_le_weak. rewrite Qabs_Qlt_condition in Hxbnd, Hzbnd |- *. rewrite Qpower_minus_pos in Hxbnd, Hzbnd. lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra