proposition: Theorem addℝ_resp_Rlt_realizer : forall e, addℝ_resp_Rlt↓e ⊩ ∀x y z, Total z → (x << y → x + z << y + z)%Re.
proof: Proof. intro. unfold Rlt at 1. Opaque Rlt. Ksolve. Ksolve. apply Qq_realizer. find. start. apply ℚdiv_realizer. find. find. assert (0 < ε/3) by now apply third_pos. start. apply Ht. find. Transparent Rlt. Kmove. exists (ε₁ + ε / 3), (ε / 3), (ε₂ + ε / 3). find. change 0 with (0 + 0). apply Qcplus_lt_compat; ok. change 0 with (0 + 0). apply Qcplus_lt_compat; ok. replace (q₁ + q + (ε₁ + ε / 3) + ε / 3 + (ε₂ + ε / 3)) with (q₁ + ε₁ + ε + ε₂ + q) by (Qcunfold; qc; field). now apply Qcplus_le_compat. unfold addℝ. Kmove. exists ε₁, (ε / 3%Z). find. unfold addℝ. Kmove. exists ε₂, (ε / 3%Z). find. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations