From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Feb 2012 11:31:22 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1927
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=f5b55b3e3395ec39a1429468ae833dbff72158c4

commit by user andrea
---

diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma
index 24cfc5ef6..226050632 100644
--- a/weblib/arithmetics/nat.ma
+++ b/weblib/arithmetics/nat.ma
@@ -552,7 +552,7 @@ monotonic_lt_plus_r. *)
 
 theorem monotonic_lt_plus_l: 
 ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a (λm.ma title="natural plus" href="cic:/fakeuri.def(1)"+/an).
-/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a/span/span/ qed.
+(* /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a/span/span/ *) #n @a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a // qed.
 
 (*
 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
@@ -945,7 +945,7 @@ qed.
 
 theorem monotonic_le_minus_r: 
 ∀p,q,n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. q a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → na title="natural minus" href="cic:/fakeuri.def(1)"-/ap a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a na title="natural minus" href="cic:/fakeuri.def(1)"-/aq.
-#p #q #n #lepq @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"le_plus_to_minus/a span class="error" title="Parse error: illegal begin of statement"/span
+#p #q #n #lepq @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"le_plus_to_minus/a 
 @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(9)"le_plus_minus_m_m/a ? q)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a/span/span/
 qed.
 
@@ -979,11 +979,11 @@ theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p).
 >associative_plus <plus_minus_m_m //
 qed.  *)
 
-theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
-  p+(n-m) = n-(m-p).
+theorem minus_minus: ∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. p a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n →
+  pa title="natural plus" href="cic:/fakeuri.def(1)"+/a(na title="natural minus" href="cic:/fakeuri.def(1)"-/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural minus" href="cic:/fakeuri.def(1)"-/a(ma title="natural minus" href="cic:/fakeuri.def(1)"-/ap).
 #n #m #p #lepm #lemn
-@sym_eq @plus_to_minus <associative_plus <plus_minus_m_m //
-<commutative_plus <plus_minus_m_m //
+@a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a @a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a <a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a <a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a //
+<a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"commutative_plus/a <a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a //
 qed.
 
 (*********************** boolean arithmetics ********************) 
@@ -991,20 +991,20 @@ include "basics/bool.ma".
 
 let rec eqb n m ≝ 
 match n with 
-  [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] 
-  | S p ⇒ match m with [ O ⇒ false | S q ⇒ eqb p q]
+  [ O ⇒ match m with [ O ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a | S q ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a] 
+  | S p ⇒ match m with [ O ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a | S q ⇒ eqb p q]
   ].
 
-theorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
-(n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). 
-@nat_elim2 
+theorem eqb_elim : ∀ n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.∀ P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.
+(na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/am → (P a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a)) → (n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m → (P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a)) → (P (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n m)). 
+@a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a 
   [#n (cases n) normalize /span class="autotactic"3span class="autotrace" trace /span/span/ 
   |normalize /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/sym_not_eq.def(4)"sym_not_eq/a/span/span/
   |normalize /span class="autotactic"4span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"not_eq_S/a/span/span/ 
   ] 
 qed.
 
-theorem eqb_n_n: ∀n. eqb n n = true.
+theorem eqb_n_n: ∀n. a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
 #n (elim n) normalize // qed. 
 
 theorem eqb_true_to_eq: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m.
@@ -1013,7 +1013,7 @@ theorem eqb_true_to_eq: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,
 theorem eqb_false_to_not_eq: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m.
 #n #m @(a href="cic:/matita/arithmetics/nat/eqb_elim.def(5)"eqb_elim/a n m) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a/span/span/ qed.
 
-theorem eq_to_eqb_true: ∀n,m:nat.n = m → eqb n m = true.
+theorem eq_to_eqb_true: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m → a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
 // qed.
 
 theorem not_eq_to_eqb_false: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
@@ -1022,15 +1022,15 @@ theorem not_eq_to_eqb_false: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind
 
 let rec leb n m ≝ 
 match n with 
-    [ O ⇒ true
+    [ O ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a
     | (S p) ⇒
 	match m with 
-        [ O ⇒ false
+        [ O ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a
 	      | (S q) ⇒ leb p q]].
 
-theorem leb_elim: ∀n,m:nat. ∀P:bool → Prop. 
-(n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
-@nat_elim2 normalize
+theorem leb_elim: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. ∀P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop. 
+(n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → P a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → (n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a m → P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → P (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m).
+@a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a normalize
   [/span class="autotactic"2span class="autotrace" trace /span/span/
   |/span class="autotactic"3span class="autotrace" trace /span/span/
   |#n #m #Hind #P #Pt #Pf @Hind
@@ -1051,7 +1051,7 @@ theorem le_to_leb_true: ∀n,m. n a title="natural 'less or equal to'" href="ci
 theorem not_le_to_leb_false: ∀n,m. n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a m → a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
 #n #m @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a // #H #H1 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed.
 
-theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false.
+theorem lt_to_leb_false: ∀n,m. m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a, a href="cic:/matita/arithmetics/nat/not_le_to_leb_false.def(7)"not_le_to_leb_false/a/span/span/ qed.
 
 (* serve anche ltb? 
@@ -1095,11 +1095,11 @@ lemma commutative_min: a href="cic:/matita/basics/relations/commutative.def(1)"
 lemma le_minr: ∀i,n,m. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/min.def(2)"min/a n m → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m.
 #i #n #m normalize @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a/span/span/ qed. 
 
-lemma le_minl: ∀i,n,m. i ≤ min n m → i ≤ n.
+lemma le_minl: ∀i,n,m. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/min.def(2)"min/a n m → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_minr.def(7)"le_minr/a/span/span/ qed.
 
-lemma to_min: ∀i,n,m. i ≤ n → i ≤ m → i ≤ min n m.
-#i #n #m #lein #leim normalize (cases (leb n m)) 
+lemma to_min: ∀i,n,m. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/min.def(2)"min/a n m.
+#i #n #m #lein #leim normalize (cases (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m)) 
 normalize // qed.
 
 lemma commutative_max: a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a ? a href="cic:/matita/arithmetics/nat/max.def(2)"max/a.
@@ -1111,7 +1111,7 @@ lemma commutative_max: a href="cic:/matita/basics/relations/commutative.def(1)"
 lemma le_maxl: ∀i,n,m. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i.
 #i #n #m normalize @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a/span/span/ qed. 
 
-lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
+lemma le_maxr: ∀i,n,m. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"le_maxl/a/span/span/ qed.
 
 lemma to_max: ∀i,n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i.