From b254cc57f5e082712f3ec6be9295eec0062b8d47 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 16 Feb 2010 07:34:33 +0000 Subject: [PATCH] Minor fixings. --- helm/software/matita/nlibrary/arithmetics/nat.ma | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma index a163960f7..6f57893a5 100644 --- a/helm/software/matita/nlibrary/arithmetics/nat.ma +++ b/helm/software/matita/nlibrary/arithmetics/nat.ma @@ -220,6 +220,9 @@ interpretation "natural 'less than'" 'lt x y = (lt x y). interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)). +(* nlemma eq_lt: ∀n,m. (n < m) = (S n ≤ m). +//; nqed. *) + ndefinition ge: nat \to nat \to Prop \def \lambda n,m:nat.m \leq n. @@ -240,8 +243,9 @@ nqed. ntheorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p \def transitive_le. *) -ntheorem transitive_lt: transitive nat lt. -#a; #b; #c; #ltab; #ltbc;nelim ltbc;/2/;nqed. + +naxiom transitive_lt: transitive nat lt. +(* #a; #b; #c; #ltab; #ltbc;nelim ltbc;/2/;nqed.*) (* theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p @@ -567,7 +571,7 @@ 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. +#a; nelim a; nnormalize; /3/; nqed. ntheorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m. /2/; nqed. -- 2.39.2