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.
[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.
|rewrite < sym_times.
rewrite > distr_times_minus.
rewrite > plus_minus
- [auto.
+ [autobatch.
(*
rewrite > sym_times.
rewrite < H5.
apply plus_to_minus.
apply H3
*)
- |auto.
+ |autobatch.
(*
apply le_times_r.
apply lt_to_le.
(* 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.