proposition: Theorem plus_assoc2_realizer : forall e, plus_assoc2↓e ⊩ ∀x y z, (x + y) + z ≤ x + (y + z).
proof: Proof. unfold Rle, Radd. do 2 Ksolve. Ksolve. Ksolve. replace (q' - q'1 - (q'0 - q'1)) with (q' - q'0) by ring. eapply sub_term. eassumption. apply (↓z). revert Hc. Qcunfold. lra. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals