proposition: Theorem addℝ_Rle_compat_realizer : forall e, addℝ_Rle_compat↓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. revert Hle₁. subst. Qcunfold. lra. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations