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