X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fdiv_and_mod_new.ma;h=f08a5f94e81f605448c63c511413091462e187f5;hb=6e61c5884aa89838a04659f90dc8d210e3703502;hp=325244f7a4708fbd3777530ed972c916721ab386;hpb=4421f312e9614e608d0ddf6fa029c761f87ceb45;p=helm.git

diff --git a/helm/software/matita/library/nat/div_and_mod_new.ma b/helm/software/matita/library/nat/div_and_mod_new.ma
index 325244f7a..f08a5f94e 100644
--- a/helm/software/matita/library/nat/div_and_mod_new.ma
+++ b/helm/software/matita/library/nat/div_and_mod_new.ma
@@ -151,7 +151,7 @@ qed.
 
 theorem div_mod_spec_div_mod: 
 \forall n,m. O < m \to (div_mod_spec n m (n / m) (n \mod m)).
-intros.auto.
+intros.autobatch.
 (*
 apply div_mod_spec_intro.
 apply lt_mod_m_m.assumption.
@@ -170,7 +170,7 @@ apply (nat_compare_elim q q1);intro
         [apply (lt_to_not_le r b H2 Hcut2)
         |elim Hcut.assumption
         ]
-      |auto depth=4. apply (trans_le ? ((q1-q)*b))
+      |autobatch depth=4. apply (trans_le ? ((q1-q)*b))
         [apply le_times_n.
          apply le_SO_minus.exact H6
         |rewrite < sym_plus.
@@ -180,7 +180,7 @@ apply (nat_compare_elim q q1);intro
     |rewrite < sym_times.
      rewrite > distr_times_minus.
      rewrite > plus_minus
-      [auto.
+      [autobatch.
        (*
        rewrite > sym_times.
        rewrite < H5.
@@ -188,7 +188,7 @@ apply (nat_compare_elim q q1);intro
        apply plus_to_minus.
        apply H3
        *)
-      |auto.
+      |autobatch.
        (*
        apply le_times_r.
        apply lt_to_le.
@@ -358,3 +358,12 @@ let rec n_divides_aux p n m acc \def
 
 (* n_divides n m = <q,r> if m divides n q times, with remainder r *)
 definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O.
+
+(*a simple variant of div_times theorem *)
+theorem div_times_ltO: \forall a,b:nat. O \lt b \to
+a*b/b = a.
+intros.
+rewrite > sym_times.
+rewrite > (S_pred b H).
+apply div_times.
+qed.