From 285a66d7ab69b1cb4b060cc9d8e4f1953095759e Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 25 Mar 2010 08:41:21 +0000 Subject: [PATCH] Conflict(?). From: asperti --- helm/software/matita/nlibrary/arithmetics/nat.ma | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma index 1ef6a81cb..f15f8cbc8 100644 --- a/helm/software/matita/nlibrary/arithmetics/nat.ma +++ b/helm/software/matita/nlibrary/arithmetics/nat.ma @@ -80,10 +80,6 @@ napply nat_elim2; #n; ##[ ncases n; /2/; ##| /3/; ##| #m; #Hind; ncases Hind;/3/; - (* - ##[/2/; ##|#H; nwhd; - napply or_introl; - napply eq_f2; /3/; *) ##] nqed. @@ -127,7 +123,7 @@ ntheorem associative_plus : associative nat plus. #n; nelim n; nnormalize; //; nqed. ntheorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a. -//; nqed. +//; nqed. ntheorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m). #n; nelim n; nnormalize; /3/; nqed. @@ -261,6 +257,9 @@ ntheorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m. ntheorem le_O_n : ∀n:nat. O ≤ n. #n; nelim n; /2/; nqed. +ntheorem nboh: 0 ≤ 0 + 0. +//; nqed. + ntheorem le_n_Sn : ∀n:nat. n ≤ S n. /2/; nqed. @@ -276,8 +275,6 @@ ntheorem monotonic_pred: monotonic ? le pred. #n; #m; #lenm; nelim lenm; /2/;nqed. ntheorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m. -(* XXX *) nletin hint ≝ monotonic. -#a; #b; #H; napplyS monotonic_pred; /2/; nqed. (* this are instances of the le versions @@ -453,9 +450,8 @@ ntheorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m → (* le and eq *) ntheorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m. -napply nat_elim2; -#n; #H1; #H2; /4/; - nqed. +napply nat_elim2; /4/; +nqed. ntheorem lt_O_S : ∀n:nat. O < S n. /2/; nqed. -- 2.39.2