From: Enrico Tassi Date: Mon, 10 Dec 2007 14:49:59 +0000 (+0000) Subject: more chosmetic X-Git-Tag: make_still_working~5712 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=43b9e1971e142d55eea8ceb57d8e6ee6d83d3791;p=helm.git more chosmetic --- diff --git a/helm/software/matita/dama/sandwich.ma b/helm/software/matita/dama/sandwich.ma index 95dd0d3cb..21499ee72 100644 --- a/helm/software/matita/dama/sandwich.ma +++ b/helm/software/matita/dama/sandwich.ma @@ -54,16 +54,16 @@ cases (H n3) (H7 H8); clear Lt_n1n3 Lt_n2n3 Lt_n1n2_n3 c H1 H2 H n1 n2; (* the main inequality *) 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) as H9; clear H7 H8; - 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 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); + lapply (le_mtri ????? H7 H8) as H9; clear H7 H8; + lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H9) as H10; clear H9; + 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;] + apply (Le≪ (δ(an n3) (xn n3)+ δ(an n3) x) (msymmetric ??(an n3)(xn n3))); + apply (Le≪ (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x) H11); apply (Le≪ (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x) (plus_comm ??(δ(an n3) (bn n3)))); apply (Le≪ (- δ(xn n3) (bn n3)+ (δ(an n3) (bn n3)+δ(an n3) x)) (plus_assoc ????)); apply (Le≪ ((δ(an n3) (bn n3)+δ(an n3) x)+- δ(xn n3) (bn n3)) (plus_comm ???));