proposition: Theorem addℝ_0_l_realizer : forall e, addℝ_0_l↓e ⊩ ∀x, Cauchy x → (x + 0 ≡ x)%Re.
proof: Proof. Ksolve. start. apply (prop_guard Ht3). intros [_ ?]. Kmove. exists ε₁0. find. now apply Qclt_le_weak. apply (prop_subst_stack Hπ). clear_realizers. subst. intro Hle. rewrite Qcplus_0_r. etransitivity. eassumption. revert Hc2. Qcunfold. lra. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations