qed.
lemma Rlt_plus_l_to_r : ∀a,b,c.a + b < c → a < c - b.
-intros; autobatch depth=4;
+intros;
+autobatch by H, (Rlt_plus_l (-b) (a+b) c);
(*
rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b);
rewrite < assoc_Rplus;
rewrite < sym_Rplus;rewrite < sym_Rplus in ⊢ (??%);
-apply Rlt_plus_l;assumption;
+apply (Rlt_plus_l (-b) (a+b) c);assumption;
*)
qed.