From a581a54f6118908a21ed3f960c70a0a2c863ca89 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 27 Jan 2010 10:29:07 +0000
Subject: [PATCH] le_arith

---
 .../matita/nlibrary/arithmetics/nat.ma        | 121 +++++++-----------
 1 file changed, 43 insertions(+), 78 deletions(-)

diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index b6683b267..287648840 100644
--- a/helm/software/matita/nlibrary/arithmetics/nat.ma
+++ b/helm/software/matita/nlibrary/arithmetics/nat.ma
@@ -559,88 +559,53 @@ ntheorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n.
 //; nqed.
 
 ntheorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m.
-#a; nelim a; /3/; nqed.
-
-(* times 
-theorem monotonic_le_times_r: 
-\forall n:nat.monotonic nat le (\lambda m. n * m).
-simplify.intros.elim n.
-simplify.apply le_O_n.
-simplify.apply le_plus.
-assumption.
-assumption.
-qed.
+#a; nelim a; /3/; nqed. 
 
-theorem le_times_r: \forall p,n,m:nat. n \le m \to p*n \le p*m
-\def monotonic_le_times_r.
+(* times *)
+ntheorem monotonic_le_times_r: 
+∀n:nat.monotonic nat le (λm. n * m).
+#n; #x; #y; #lexy; nelim n; nnormalize;//;
+#a; #lea; napply le_plus;//; (* lentissimo /2/ *)
+nqed.
 
-theorem monotonic_le_times_l: 
-\forall m:nat.monotonic nat le (\lambda n.n*m).
-simplify.intros.
-rewrite < sym_times.rewrite < (sym_times m).
-apply le_times_r.assumption.
-qed.
+(*
+ntheorem le_times_r: \forall p,n,m:nat. n \le m \to p*n \le p*m
+\def monotonic_le_times_r. *)
 
-theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p
-\def monotonic_le_times_l.
+ntheorem monotonic_le_times_l: 
+∀m:nat.monotonic nat le (λn.n*m).
+/2/; nqed.
 
-theorem le_times: \forall n1,n2,m1,m2:nat. n1 \le n2  \to m1 \le m2 
-\to n1*m1 \le n2*m2.
-intros.
-apply (trans_le ? (n2*m1)).
-apply le_times_l.assumption.
-apply le_times_r.assumption.
-qed.
+(*
+theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p
+\def monotonic_le_times_l. *)
+
+ntheorem le_times: ∀n1,n2,m1,m2:nat. 
+n1 ≤ n2  → m1 ≤ m2 → n1*m1 ≤ n2*m2.
+#n1; #n2; #m1; #m2; #len; #lem; 
+napply transitive_le; (* too slow *)
+ ##[ ##| napply monotonic_le_times_l;//; 
+     ##| napply monotonic_le_times_r;//;
+ ##]
+nqed.
 
-theorem le_times_n: \forall n,m:nat.(S O) \le n \to m \le n*m.
-intros.elim H.simplify.
-elim (plus_n_O ?).apply le_n.
-simplify.rewrite < sym_plus.apply le_plus_n.
-qed.
+ntheorem lt_times_n: ∀n,m:nat. O < n → m ≤ n*m.
+(* bello *)
+/2/; nqed.
 
-theorem le_times_to_le: 
-\forall a,n,m. S O \le a \to a * n \le a * m \to n \le m.
-intro.
-apply nat_elim2;intros
-  [apply le_O_n
-  |apply False_ind.
-   rewrite < times_n_O in H1.
-   generalize in match H1.
-   apply (lt_O_n_elim ? H).
-   intros.
-   simplify in H2.
-   apply (le_to_not_lt ? ? H2).
-   apply lt_O_S
-  |apply le_S_S.
-   apply H
-    [assumption
-    |rewrite < times_n_Sm in H2.
-     rewrite < times_n_Sm in H2.
-     apply (le_plus_to_le a).
-     assumption
-    ]
-  ]
-qed.
+ntheorem le_times_to_le: 
+∀a,n,m. O < a → a * n ≤ a * m → n ≤ m.
+#a; napply nat_elim2; nnormalize;
+  ##[//;
+  ##|#n; #H1; #H2; napply False_ind;
+     ngeneralize in match H2;
+     napply lt_to_not_le;
+     napply (transitive_le ? (S n));/2/;
+  ##|#n; #m; #H; #lta; #le;
+     napply le_S_S; napply H; /2/;
+  ##]
+nqed.
 
-theorem le_S_times_SSO: \forall n,m.O < m \to
-n \le m \to S n \le (S(S O))*m.
-intros.
-simplify.
-rewrite > plus_n_O.
-simplify.rewrite > plus_n_Sm.
-apply le_plus
-  [assumption
-  |rewrite < plus_n_O.
-   assumption
-  ]
-qed.
-(*0 and times *)
-theorem O_lt_const_to_le_times_const:  \forall a,c:nat.
-O \lt c \to a \le a*c.
-intros.
-rewrite > (times_n_SO a) in \vdash (? % ?).
-apply le_times
-[ apply le_n
-| assumption
-]
-qed. *)
\ No newline at end of file
+ntheorem le_S_times_2: ∀n,m.O < m → n ≤ m → n < 2*m.
+#n; #m; #posm; #lenm; (* interessante *)
+nnormalize; napplyS (le_plus n); //; nqed.
-- 
2.39.2