qed. *)
lemma Rtimes_x_R0 : ∀x.x * R0 = R0.
-intro; autobatch paramodulation.
-(*
+(*intro; autobatch paramodulation.*)
+intros;
rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
rewrite < (Rplus_Ropp (x*R0)) in ⊢ (? ? (? ? %) %);
rewrite < assoc_Rplus;
apply eq_f2;autobatch paramodulation;
-*)
+
qed.
lemma eq_Rtimes_Ropp_R1_Ropp : ∀x.x*(-R1) = -x.
-intro. autobatch paramodulation. (*
-auto paramodulation.
+intro. (*autobatch paramodulation.*)
+
rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
rewrite < Rplus_x_R0 in ⊢ (? ? ? %);
rewrite < (Rplus_Ropp x) in ⊢ (? ? % ?);
apply eq_f2 [reflexivity]
rewrite < Rtimes_x_R1 in ⊢ (? ? (? % ?) ?);
rewrite < distr_Rtimes_Rplus_l;autobatch paramodulation;
-*)
+
qed.
lemma Ropp_inv : ∀x.x = Ropp (Ropp x).
lemma Rlt_plus_l_to_r : ∀a,b,c.a + b < c → a < c - b.
intros;
-(* cut (∀x,y.x+(-x+y) = y);[2:
-intros.demodulate all.]
-applyS (Rlt_plus_l c (-?+a) (-b) ?) by (Hcut c a);
- [2: applyS Hletin;
-lapply (Rlt_plus_l (-b) ?? H); autobatch; applyS Hletin; *)
+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.
lemma Rlt_plus_r_to_l : ∀a,b,c.a < b + c → a - c < b.