other addition to the standard library removed

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
index 2b8f3f9535ba442e2fda7f3e7cdfb4a9aa7e606d..9d085fc0566f9d508f2d9a5214dea9be09bf6514 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
@@ -183,7 +183,7 @@ qed-.
 
 lemma ldrop_fwd_lw: ∀L1,L2,d,e. ↓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1].
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize
-[ /2 width=1/
+[ /2 width=3/
 | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
   >(tw_lift … HV21) -HV21 /2 width=1/
 ]

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma
index 3f5b8ab6a9e3a48af758f799267d18592c9e3f15..cfcf976e00bbfd07dc73e8d9d2e1ac59c3e56699 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma
@@ -126,7 +126,7 @@ theorem lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
   elim (lift_inv_lref1 … HX) -HX * #Hid2 #HX destruct /3 width=3/ /4 width=3/
 | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hd21
   lapply (transitive_le … Hd21 Hid1) -Hd21 #Hid2
-  lapply (lift_inv_lref1_ge … HX ?) -HX /2 width=1/ #HX destruct
+  lapply (lift_inv_lref1_ge … HX ?) -HX /2 width=3/ #HX destruct
   >plus_plus_comm_23 /4 width=3/
 | #p #d1 #e1 #d2 #e2 #X #HX #_
   >(lift_inv_gref1 … HX) -HX /2 width=3/

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma
index 6e3565e731f6a26db60c5b4fe7973bce62bc8f16..aaecbbf3b4acfe2084ccd75cef48c0ad8b0eac1a 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma
@@ -168,10 +168,11 @@ lemma tps_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
     elim (lift_trans_le … HUV … HVW ?) -V // >minus_plus <plus_minus_m_m // -Hid /3 width=4/
   | -Hdti -Hdedet
     lapply (transitive_le … (i - e) Hdtd ?) /2 width=1/ -Hdtd #Hdtie
-    elim (le_inv_plus_l … Hid) #_ #Hei
+    elim (le_inv_plus_l … Hid) #Hdie #Hei
     lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV
-    elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid
-    #V1 #HV1 >plus_minus // <minus_minus // /2 width=1/ /4 width=4/
+    elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid -Hdie
+    #V1 #HV1 >plus_minus // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O #H
+    @ex2_1_intro [3: @H | skip | @tps_subst [3,5,6: // |1,2: skip | >commutative_plus >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *)
   ]
 | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
@@ -199,12 +200,12 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
 | #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt
   lapply (transitive_le … Hdedt … Hdti) #Hdei
   elim (le_inv_plus_l … Hdedt) -Hdedt #_ #Hedt
-  elim (le_inv_plus_l … Hdei) #_ #Hei
+  elim (le_inv_plus_l … Hdei) #Hdie #Hei
   lapply (lift_inv_lref2_ge … H … Hdei) -H #H destruct
   lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV
-  elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hdei 
-  #V0 #HV10 >plus_minus // <minus_minus // /2 width=1/ #HV02
-  @ex2_1_intro /3 width=4/ (**) (* explicitc constructors *)
+  elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hdei -Hdie 
+  #V0 #HV10 >plus_minus // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O #H
+  @ex2_1_intro [3: @H | skip | @tps_subst [5,6: // |1,2: skip | /2 width=1/ | >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *)
 | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
   elim (le_inv_plus_l … Hdetd) #_ #Hedt

diff --git a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
index 5d14a43dd826869dc5bb99554bc8d06a9201cfb5..80e23e6956a2ea78bccda3a080348a853774207b 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
@@ -28,6 +28,9 @@ lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
 lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
 /2 by plus_minus/ qed.
 
+lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
+ /3 by monotonic_le_minus_l, le_to_le_to_eq/ qed.
+
 lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
 #b elim b -b
 [ #c #a #H >(le_n_O_to_eq … H) -H //
@@ -38,11 +41,8 @@ lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
 ]
 qed.
 
-lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
-/3 by monotonic_le_minus_l, le_to_le_to_eq/ qed.
-
 lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
-#a #b #c1 #H >minus_plus @eq_f2 /2 width=1/
+#a #b #c1 #H >minus_plus /3 width=1/
 qed.
 
 lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
@@ -110,100 +110,3 @@ lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2
 | #m1 #_ #IHm1 #n1 #n2 #H @IHm1 /2 width=3/
 ]
 qed-.
-
-(* backward lemmas **********************************************************)
-
-lemma monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
-#p #q #n #H1 #H2
-@lt_plus_to_minus_r <plus_minus_m_m //.
-qed.
-
-(* unstable *****************************************************************)
-
-lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
-#j #i #e #d #H lapply (le_plus_to_minus_r … H) -H /2 width=3/
-qed.
-
-lemma arith5: ∀a,b1,b2,c1. c1 ≤ b1 → c1 ≤ a → a < b1 + b2 → a - c1 < b1 - c1 + b2.
-#a #b1 #b2 #c1 #H1 #H2 #H3
->plus_minus // @monotonic_lt_minus_l //
-qed.
-
-lemma arith10: ∀a,b,c,d,e. a ≤ b → c + (a - d - e) ≤ c + (b - d - e).
-#a #b #c #d #e #H
->minus_plus >minus_plus @monotonic_le_plus_r @monotonic_le_minus_l //
-qed.
-
-(* remove *******************************************************************)
-(*
-lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
-// qed.
-
-lemma plus_S_le_to_pos: ∀n,m,p. n + S m ≤ p → 0 < p.
-/2 by ltn_to_ltO/ qed.
-
-lemma minus_le: ∀m,n. m - n ≤ m.
-/2 by monotonic_le_minus_l/ qed.
-
-lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
-/2 by le_n_O_to_eq/ qed.
-
-lemma lt_to_le: ∀a,b. a < b → a ≤ b.
-/2 by le_plus_b/ qed.
-
-lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n.
-/2 by le_to_or_lt_eq/ qed.
-
-lemma plus_le_weak: ∀m,n,p. m + n ≤ p → n ≤ p.
-/2 by le_plus_b/ qed.
-
-lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
-/2 by le_plus_to_minus_r/ qed.
-
-lemma lt_plus_minus: ∀i,u,d. u ≤ i → i < d + u → i - u < d.
-/2 by monotonic_lt_minus_l/ qed.
-
-lemma arith_a2: ∀a,c1,c2. c1 + c2 ≤ a → a - c1 - c2 + (c1 + c2) = a.
-/2 by plus_minus/ qed.
-
-lemma arith_c1: ∀a,b,c1. a + c1 - (b + c1) = a - b.
-// qed.
-
-lemma arith_d1: ∀a,b,c1. c1 ≤ b → a + c1 + (b - c1) = a + b.
-/2 by plus_minus/ qed.
-
-lemma arith_e2: ∀a,c1,c2. a ≤ c1 → c1 + c2 - (c1 - a + c2) = a.
-/2 by minus_le_minus_minus_comm/ qed.
-
-lemma arith_f1: ∀a,b,c1. a + b ≤ c1 → c1 - (c1 - a - b) = a + b.
-/2 by minus_le_minus_minus_comm/
-qed.
-
-lemma arith_g1: ∀a,b,c1. c1 ≤ b → a - (b - c1) - c1 = a - b.
-/2 by arith_b1/ qed.
-
-lemma arith_i2: ∀a,c1,c2. c1 + c2 ≤ a → c1 + c2 + (a - c1 - c2) = a.
-/2 by plus_minus_m_m/ qed.
-
-lemma arith_z1: ∀a,b,c1. a + c1 - b - c1 = a - b.
-// qed.
-
-lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
-/2 by le_plus_to_le/ qed.
-
-lemma arith3: ∀a1,a2,b,c1. a1 + a2 ≤ b → a1 + c1 + a2 ≤ b + c1.
-/2 by le_minus_to_plus/ qed.
-
-lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
-/2 by arith3/ qed.
-
-lemma arith8: ∀a,b. a < a + b + 1.
-// qed.
-
-lemma arith9: ∀a,b,c. c < a + (b + c + 1) + 1.
-// qed.
-
-(* backward form of le_inv_plus_l *)
-lemma P2: ∀x,y,z. x ≤ z - y → y ≤ z → x + y ≤ z.
-/2 by le_minus_to_plus_r/ qed.
-*)