From 9cc54d0dfa73c0b7e2936d80fe9466269d81d9c4 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 19 Feb 2010 07:25:04 +0000 Subject: [PATCH] --- helm/software/matita/nlibrary/arithmetics/nat.ma | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma index 6f57893a5..120a0bb16 100644 --- a/helm/software/matita/nlibrary/arithmetics/nat.ma +++ b/helm/software/matita/nlibrary/arithmetics/nat.ma @@ -112,7 +112,7 @@ ntheorem plus_Sn_m1: ∀n,m:nat. S m + n = n + S m. #n; nelim n; nnormalize; //; nqed. *) -(* +(* deleterio ntheorem plus_n_SO : ∀n:nat. S n = n+S O. //; nqed. *) @@ -293,9 +293,11 @@ ntheorem not_le_to_not_le_S_S: ∀ n,m:nat. n ≰ m → S n ≰ S m. ntheorem not_le_S_S_to_not_le: ∀ n,m:nat. S n ≰ S m → n ≰ m. /3/; nqed. +naxiom decidable_le: ∀n,m. decidable (n≤m). +(* ntheorem decidable_le: ∀n,m. decidable (n≤m). napply nat_elim2; #n; /3/; -#m; #dec; ncases dec;/4/; nqed. +#m; #dec; ncases dec;/4/; nqed. *) ntheorem decidable_lt: ∀n,m. decidable (n < m). #n; #m; napply decidable_le ; nqed. @@ -558,7 +560,7 @@ ntheorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p ntheorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2 \to m1 ≤ m2 → n1 + m1 ≤ n2 + m2. -#n1; #n2; #m1; #m2; #len; #lem; napply transitive_le; +#n1; #n2; #m1; #m2; #len; #lem; napply (transitive_le ? (n1+m2)); /2/; nqed. ntheorem le_plus_n :∀n,m:nat. m ≤ n + m. @@ -639,7 +641,7 @@ napply transitive_le; (* /2/ slow *) nqed. ntheorem lt_times_n: ∀n,m:nat. O < n → m ≤ n*m. -(* bello *) +#n; #m; #H; napplyS monotonic_le_times_l; /2/; nqed. ntheorem le_times_to_le: @@ -655,9 +657,9 @@ ntheorem le_times_to_le: ##] nqed. -ntheorem le_S_times_2: ∀n,m.O < m → n ≤ m → n < 2*m. +ntheorem le_S_times_2: ∀n,m.O < m → n ≤ m → S n ≤ 2*m. #n; #m; #posm; #lenm; (* interessante *) -nnormalize; napplyS (le_plus n); //; nqed. +napplyS (le_plus n); //; nqed. (* times & lt *) (* -- 2.39.2