proposition: Theorem plus_comm_realizer : forall x y, forall e, (λ"_" λ"_" λ"x" λ"f" "x" @ (swap @ "f"))↓e ⊩ x+y ≤ y+x.
proof: Proof. unfold Rle, Radd, swap. do 2 Ksolve. replace (q' - (q - q'0)) with (q'0 + (q' - q))%Qc by ring. eapply sub_term. eassumption. apply (↓x). revert Hc. Qcunfold. lra. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals