-lemma Rle_plus_r : ∀x,y,z:R.x ≤ y → x + z ≤ y + z.
-intros;
-applyS Rle_plus_l;
-autobatch;
-(*rewrite > sym_Rplus;rewrite > sym_Rplus in ⊢ (??%);*)
-(*applyS Rle_plus_l;
-applyS*)
-cut ((x+z ≤ y+z) = (λx.(x+?≤ x+?)) ?);[5:simplify;
- demodulate all;
- autobatch paramodulation by sym_Rplus;
-
-applyS Rle_plus_l by sym_Rplus;
-
-cut ((x ≤ y) = (x+z ≤ y+z)); [2:
- lapply (Rle_plus_l ?? z H);
- autobatch paramodulation by sym_Rplus,Hletin;