More exceptions pretty-printed.

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

diff --git a/helm/software/matita/library/nat/lt_arith.ma b/helm/software/matita/library/nat/lt_arith.ma
index f60da5eba31f2c07d7b53c70d62c231d362c2208..f0fdbdbd6d6cf9aeecba4b23c6b96d9ea270a735 100644 (file)
--- a/helm/software/matita/library/nat/lt_arith.ma
+++ b/helm/software/matita/library/nat/lt_arith.ma
@@ -30,7 +30,7 @@ monotonic_lt_plus_r.
 
 theorem monotonic_lt_plus_l: 
 \forall n:nat.monotonic nat lt (\lambda m.m+n).
-change with (\forall n,p,q:nat. p < q \to p + n < q + n).
+simplify.
 intros.
 rewrite < sym_plus. rewrite < (sym_plus n).
 apply lt_plus_r.assumption.
@@ -71,10 +71,9 @@ qed.
 (* times *)
 theorem monotonic_lt_times_r: 
 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
-change with (\forall n,p,q:nat. p < q \to (S n) * p < (S n) * q).
+simplify.
 intros.elim n.
 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
-change with (p + (S n1) * p < q + (S n1) * q).
 apply lt_plus.assumption.assumption.
 qed.
 
@@ -83,10 +82,9 @@ theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
 
 theorem monotonic_lt_times_l: 
 \forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
-change with 
-(\forall n,p,q:nat. p < q \to p*(S n) < q*(S n)).
+simplify.
 intros.
-rewrite < sym_times.rewrite < (sym_times (S n)).
+rewrite < sym_times.rewrite < (sym_times (S m)).
 apply lt_times_r.assumption.
 qed.
 
@@ -113,6 +111,28 @@ assumption.
 apply (ltn_to_ltO p q H2).
 qed.
 
+theorem lt_times_r1: 
+\forall n,m,p. O < n \to m < p \to n*m < n*p.
+intros.
+elim H;apply lt_times_r;assumption.
+qed.
+
+theorem lt_times_l1: 
+\forall n,m,p. O < n \to m < p \to m*n < p*n.
+intros.
+elim H;apply lt_times_l;assumption.
+qed.
+
+theorem lt_to_le_to_lt_times : 
+\forall n,n1,m,m1. n < n1 \to m \le m1 \to O < m1 \to n*m < n1*m1.
+intros.
+apply (le_to_lt_to_lt ? (n*m1))
+  [apply le_times_r.assumption
+  |apply lt_times_l1
+    [assumption|assumption]
+  ]
+qed.
+
 theorem lt_times_to_lt_l: 
 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
 intros.
@@ -128,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.
@@ -137,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.