proposition: Lemma CReal_plus_opp_r : forall x : CReal, x + - x == 0.
proof: Proof. intros x; apply CRealEq_diff; intros n. unfold CReal_plus, CReal_plus_seq, CReal_opp, CReal_opp_seq, inject_Q. do 3 rewrite CReal_red_seq. rewrite Qred_correct. pose proof ((cauchy x) (n)%Z (n-1)%Z (n)%Z ltac:(lia) ltac:(lia)) as Hxbnd. apply Qlt_le_weak. rewrite Qabs_Qlt_condition in Hxbnd |- *. lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra