X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Flt_arith.ma;h=a568ca408be94412a0203a82abf170709edfaa05;hb=b58315ef220a130a44acbf528cd6885ddadad642;hp=cce6626a0f43d9273c23a2be0ea6fa90fd55a105;hpb=6d49a181a1b771f797d37b02661b5743aee86ac1;p=helm.git

diff --git a/helm/software/matita/library/nat/lt_arith.ma b/helm/software/matita/library/nat/lt_arith.ma
index cce6626a0..a568ca408 100644
--- a/helm/software/matita/library/nat/lt_arith.ma
+++ b/helm/software/matita/library/nat/lt_arith.ma
@@ -262,6 +262,26 @@ apply lt_to_not_eq.assumption.
 intro.reflexivity.
 qed.
 
+(* times and plus *)
+theorem lt_times_plus_times: \forall a,b,n,m:nat. 
+a < n \to b < m \to a*m + b < n*m.
+intros 3.
+apply (nat_case n)
+  [intros.apply False_ind.apply (not_le_Sn_O ? H)
+  |intros.simplify.
+   rewrite < sym_plus.
+   unfold.
+   change with (S b+a*m1 \leq m1+m*m1).
+   apply le_plus
+    [assumption
+    |apply le_times
+      [apply le_S_S_to_le.assumption
+      |apply le_n
+      ]
+    ]
+  ]
+qed.
+
 (* div *) 
 
 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.