X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Flt_arith.ma;h=f0fdbdbd6d6cf9aeecba4b23c6b96d9ea270a735;hb=562e9adf40098e11d8f0bc2711a7f665360c2231;hp=b01bd546103e27247ec9797676a4983befd92584;hpb=e95f5d784fe7830fe9ed10b3e782ef2206fea896;p=helm.git

diff --git a/matita/library/nat/lt_arith.ma b/matita/library/nat/lt_arith.ma
index b01bd5461..f0fdbdbd6 100644
--- a/matita/library/nat/lt_arith.ma
+++ b/matita/library/nat/lt_arith.ma
@@ -148,6 +148,15 @@ assumption.
 exact (decidable_lt p q).
 qed.
 
+theorem lt_times_n_to_lt: 
+\forall n,p,q:nat. O < n \to p*n < q*n \to p < q.
+intro.
+apply (nat_case n)
+  [intros.apply False_ind.apply (not_le_Sn_n ? H)
+  |intros 4.apply lt_times_to_lt_l
+  ]
+qed.
+
 theorem lt_times_to_lt_r: 
 \forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
 intros.
@@ -157,6 +166,15 @@ rewrite < (sym_times (S n)).
 assumption.
 qed.
 
+theorem lt_times_n_to_lt_r: 
+\forall n,p,q:nat. O < n \to n*p < n*q \to lt p q.
+intro.
+apply (nat_case n)
+  [intros.apply False_ind.apply (not_le_Sn_n ? H)
+  |intros 4.apply lt_times_to_lt_r
+  ]
+qed.
+
 theorem nat_compare_times_l : \forall n,p,q:nat. 
 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
 intros.apply nat_compare_elim.intro.