proposition: Theorem addℝ_proper_realizer : forall e, addℝ_proper↓e ⊩ ∀x₁ x₂ y₁ y₂, (x₁ ≡ x₂ → y₁ ≡ y₂ → x₁ + y₁ ≡ x₂ + y₂)%Re.
proof: Proof. do 2 Ksolve. startn 7. eapply prop_guard. Kmove. exists ε₁0, ε₁1. Ksolve; now apply Qclt_le_weak. intro Hle₁. Kmove. repeat eexists; try eok || now apply Qclt_le_weak. apply (prop_subst_stack Hπ). clear_realizers. subst. intro Hle₂. replace (q₁0 + q₂0 - (q₁1 + q₂1)) with (q₁0 - q₁1 + (q₂0 - q₂1)) by ring. replace (ε₁0 + ε₂0 + (ε₁1 + ε₂1)) with (ε₁0 + ε₁1 + (ε₂0 + ε₂1)) by ring. etransitivity. apply Qcabs_triangle. now apply Qcplus_le_compat. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations