proposition: Lemma CReal_plus_0_l : forall r : CReal, inject_Q 0 + r == r.
proof: Proof. intros x; apply CRealEq_diff; intros n. unfold CReal_plus, CReal_plus_seq, inject_Q. do 2 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