X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fsandwich.ma;h=68bb4453cda61ce94e5aace6e3a40a8994ea3302;hb=ddc91018331d65f4c43b7c051c6fd07b614ea46b;hp=df66b8b8cb15e787d5cd814aa238fed0170e37c0;hpb=cb4d4678ada706caaf8c54f2d6780c228645f911;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/sandwich.ma b/helm/software/matita/contribs/dama/dama/sandwich.ma
index df66b8b8c..68bb4453c 100644
--- a/helm/software/matita/contribs/dama/dama/sandwich.ma
+++ b/helm/software/matita/contribs/dama/dama/sandwich.ma
@@ -33,15 +33,14 @@ cases (us_phi3 ? ? Gv) (W GW); cases GW (Gw HW); clear GW;
 cases (H1 ? Gw) (ma Hma); cases (H2 ? Gw) (mb Hmb); clear H1 H2;
 exists [apply (ma + mb)] intros; apply (HV 〈l,(x i)〉); 
 unfold; simplify; exists [apply (a i)] split;
-[2: apply (ous_convex ?? Gv 〈a i,b i〉); cases (H i) (Lax Lxb); clear H;
+[2: apply (ous_convex_l ?? Gv 〈a i,b i〉); cases (H i) (Lax Lxb); clear H;
     [1: apply HW; exists [apply l]simplify; split; 
         [1: cases (us_phi4 ?? Gw 〈(a i),l〉); apply H2; clear H2 H;
             apply (Hma i); rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;
         |2: apply Hmb; apply (le_w_plus ma); assumption] 
-    |2: simplify; apply (le_transitive ???? Lax Lxb);
-    |3: simplify; repeat split; try assumption; 
-        [1: apply (le_transitive ???? Lax Lxb);
-        |2: (* prove le_reflexive *) intro X; cases (os_coreflexive ?? X)]]
+    |2,3: simplify; apply (le_transitive (a i) ?? Lax Lxb);
+    |4: apply (le_reflexive);
+    |5,6: assumption;]
 |1: apply HW; exists[apply l] simplify; split;
     [1: apply (us_phi1 ?? Gw); unfold; apply eq_reflexive;
     |2: apply Hma;  rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;]]