refactoring of some lemmas, shorter proofs

[helm.git] / helm / software / matita / dama / sandwich.ma

diff --git a/helm/software/matita/dama/sandwich.ma b/helm/software/matita/dama/sandwich.ma
index c83136c770c85efc844c5529dc82b723b75215ce..10b54b3e4eeb7dbcdf12312569e7b9c61c55d3ad 100644 (file)
--- a/helm/software/matita/dama/sandwich.ma
+++ b/helm/software/matita/dama/sandwich.ma
@@ -36,13 +36,13 @@ cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 3) 0;
 cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 2) 0; simplify;
 intro H3;
 cut (0<w1) as H4; [2: 
-  apply (ltpow_lt ??? 2); apply (lt_rewr ???? H2);
-  apply (lt_rewl ???? (powzero ? 3)); assumption]
+  apply (ltmul_lt ??? 2); apply (lt_rewr ???? H2);
+  apply (lt_rewl ???? (mulzero ? 3)); assumption]
 cut (0<w) as H5; [2:
-  apply (ltpow_lt ??? 3); apply (lt_rewr ???? H1);
-  apply (lt_rewl ???? (powzero ? 4)); assumption]
+  apply (ltmul_lt ??? 3); apply (lt_rewr ???? H1);
+  apply (lt_rewl ???? (mulzero ? 4)); assumption]
 cut (w<w1) as H6; [2: 
-  apply (poweqplus_lt ??? 2 O); try assumption; apply (Eq≈ ? H2 H1);]
+  apply (muleqplus_lt ??? 2 O); try assumption; apply (Eq≈ ? H2 H1);]
 apply (plus_cancr_lt ??? w1);
 apply (lt_rewl ??? (w+e)); [
   apply (Eq≈ (w+3*w1) ? H2);
@@ -77,47 +77,37 @@ constructor 1; [apply (n1 + n2);] intros (n3 Hn3);
 lapply (ltwr ??? Hn3) as Hn1n3; lapply (ltwl ??? Hn3) as Hn2n3;
 elim (H1 ? Hn1n3) (H3 H4); elim (H2 ? Hn2n3) (H5 H6); clear Hn1n3 Hn2n3;
 elim (H n3) (H7 H8); clear H H1 H2; 
-lapply (le_to_eqm ??? H7) as Dxm; lapply (le_to_eqj ??? H7) as Dym;
+lapply (le_to_eqm ??? H7) as Dxm; lapply (le_to_eqj ??? H7) as Dym; 
 (* the main step *)
-cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x); [2:
+cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x) as main_ineq; [2:
   apply (le_transitive ???? (mtineq ???? (an n3)));
-  lapply (le_mtri ????? H7 H8);
-  lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? Hletin);
-  cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))); [2:
+  lapply (le_mtri ????? H7 H8) as H9;
+  lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H9) as H10; clear H9;
+  cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))) as H11; [2:
     apply (Eq≈  (0 + δ(an n3) (xn n3)) ? (zero_neutral ??));
     apply (Eq≈  (δ(an n3) (xn n3) + 0) ? (plus_comm ???));
     apply (Eq≈  (δ(an n3) (xn n3) +  (-δ(xn n3) (bn n3) +  δ(xn n3) (bn n3))) ? (opp_inverse ??));
     apply (Eq≈  (δ(an n3) (xn n3) +  (δ(xn n3) (bn n3) + -δ(xn n3) (bn n3))) ? (plus_comm ?? (δ(xn n3) (bn n3))));
-    apply (Eq≈  ? ? (eq_sym ??? (plus_assoc ????))); assumption;] clear Hletin1;
-  apply (le_rewl ???  ( δ(an n3) (xn n3)+ δ(an n3) x));[
-    apply feq_plusr; apply msymmetric;]
-  apply (le_rewl ???  (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x));[
-    apply feq_plusr; assumption;]
-  clear Hcut Hletin Dym Dxm H8 H7 H6 H5 H4 H3;
-  apply (le_rewl ??? (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x));[
-    apply feq_plusr; apply plus_comm;]
+    apply (Eq≈  ? ? (eq_sym ??? (plus_assoc ????))); assumption;] clear H10;
+  apply (le_rewl ???  ( δ(an n3) (xn n3)+ δ(an n3) x) (msymmetric ??(an n3)(xn n3)));    
+  apply (le_rewl ???  (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x) H11);
+  clear Dym Dxm H8 H7 H6 H5 H4 H3;
+  apply (le_rewl ??? (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x) (plus_comm ??(δ(an n3) (bn n3))));
   apply (le_rewl ??? (- δ(xn n3) (bn n3)+ (δ(an n3) (bn n3)+δ(an n3) x)) (plus_assoc ????));
   apply (le_rewl ??? ((δ(an n3) (bn n3)+δ(an n3) x)+- δ(xn n3) (bn n3)) (plus_comm ???));
   apply lew_opp; [apply mpositive] apply fle_plusr;
   apply (le_rewr ???? (plus_comm ???));
   apply (le_rewr ??? ( δ(an n3) x+ δx (bn n3)) (msymmetric ????));
   apply mtineq;]
-split; [
+split; [ (* first the trivial case *)
   apply (lt_le_transitive ????? (mpositive ????));
-  split; elim He; [apply  le_zero_x_to_le_opp_x_zero; assumption;]
-  cases t1; [ 
-    left; apply exc_zero_opp_x_to_exc_x_zero;
-    apply (Ex≫ ? (eq_opp_opp_x_x ??));assumption;]
-  right;  apply exc_opp_x_zero_to_exc_zero_x;
-  apply (Ex≪ ? (eq_opp_opp_x_x ??)); assumption;]
-clear Dxm Dym H7 H8 Hn3 H5 H3 n1 n2;
+  apply lt_zero_x_to_lt_opp_x_zero; assumption;]  
+clear Dxm Dym H7 H8 Hn3 H5 H3 n1 n2; cases H4 (H7 H8); clear H4;
 apply (le_lt_transitive ???? ? (sandwich_ineq ?? He));
-apply (le_transitive ???? Hcut);
+apply (le_transitive ???? main_ineq);
 apply (le_transitive ??  (e/3+ δ(an n3) x+ δ(an n3) x)); [
   repeat apply fle_plusr; cases H6; assumption;]
-apply (le_transitive ??  (e/3+ e/2 + δ(an n3) x)); [
-  apply fle_plusr; apply fle_plusl; cases H4; assumption;]
-apply (le_transitive ??  (e/3+ e/2 + e/2)); [
-  apply fle_plusl; cases H4; assumption;]
+apply (le_transitive ??  (e/3+ e/2 + δ(an n3) x) ); [apply fle_plusr; apply fle_plusl; assumption]
+apply (le_transitive ??  (e/3+ e/2 + e/2)); [apply fle_plusl; assumption;]
 apply le_reflexive;
 qed.