completed use of \mod and / notation

[helm.git] / helm / matita / library / nat / lt_arith.ma

diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index a2e7f6109af689edeb6e87fe5f09345e4ea706f8..ce66decaa1fb1f51d1bea31db0c6f908737b1849 100644 (file)
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -162,11 +162,11 @@ qed.
 
 (* div *) 
 
-theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to mod n m = O \to O < div n m. 
+theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to n \mod m = O \to O < n / m. 
 intros 4.apply lt_O_n_elim m H.intros.
 apply lt_times_to_lt_r m1.
 rewrite < times_n_O.
-rewrite > plus_n_O ((S m1)*(div n (S m1))).
+rewrite > plus_n_O ((S m1)*(n / (S m1))).
 rewrite < H2.
 rewrite < sym_times.
 rewrite < div_mod.
@@ -175,13 +175,13 @@ assumption.
 simplify.apply le_S_S.apply le_O_n.
 qed.
 
-theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to div n m \lt n.
+theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
 intros.
-apply nat_case1 (div n m).intro.
+apply nat_case1 (n / m).intro.
 assumption.intros.rewrite < H2.
 rewrite > (div_mod n m) in \vdash (? ? %).
-apply lt_to_le_to_lt ? ((div n m)*m).
-apply lt_to_le_to_lt ? ((div n m)*(S (S O))).
+apply lt_to_le_to_lt ? ((n / m)*m).
+apply lt_to_le_to_lt ? ((n / m)*(S (S O))).
 rewrite < sym_times.
 rewrite > H2.
 simplify.