From: Andrea Asperti Date: Wed, 27 Jan 2010 10:29:07 +0000 (+0000) Subject: le_arith X-Git-Tag: make_still_working~3089 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a581a54f6118908a21ed3f960c70a0a2c863ca89;p=helm.git le_arith --- 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.