From: Andrea Asperti Date: Wed, 27 Jun 2012 09:32:02 +0000 (+0000) Subject: removed a duplicate X-Git-Tag: make_still_working~1629 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7163f2ff5eb4960162d2fcf135f031ae2a9f8b56;p=helm.git removed a duplicate --- diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma index cc6b19deb..649108f47 100644 --- a/matita/matita/lib/arithmetics/nat.ma +++ b/matita/matita/lib/arithmetics/nat.ma @@ -242,7 +242,7 @@ theorem monotonic_le_plus_l: theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2 → m1 ≤ m2 → n1 + m1 ≤ n2 + m2. #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2)) -/2/ qed-. +/2/ qed. theorem le_plus_n :∀n,m:nat. m ≤ n + m. /2/ qed. @@ -595,8 +595,10 @@ theorem increasing_to_le: ∀f:nat → nat. @(ex_intro ?? (S a)) /2/ qed. +(* thus is le_plus lemma le_plus_compatible: ∀x1,x2,y1,y2. x1 ≤ y1 → x2 ≤ y2 → x1 + x2 ≤ y1 + y2. -/3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed. +#x1 #y1 #x2 #y2 #H1 #H2 /2/ @le_plus // /2/ /3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed. +*) (* lt *)