seg_u/l were inverted, more work

[helm.git] / helm / software / matita / contribs / dama / dama / property_sigma.ma

diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma
index 9d9485f9c41c84eb6b595472ff6b5eaaa6f730a6..74f03de4c9fe2ee552a207c79b15c5413fe85962 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/property_sigma.ma
+++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma
@@ -95,17 +95,19 @@ cut (⌊x,a (m x)⌋ ↑ l ∨ ⌊x,a (m x)⌋ ↓ l) as H10; [2:
  | right; apply (selection_downarrow ? Hm a l H4);]] 
 lapply (H9 ?? H10) as H11; [
   exists [apply (m 0:nat)] intros;
-  cases H1;
-    [cases H5; cases H7; apply (ous_convex ?? H3 ? H11 (H12 (m O)));
-    |cases H5; cases H7; cases (us_phi4 ?? H3 〈(a (m O)),l〉); 
-     lapply (H14 H11) as H11'; apply (ous_convex ?? H3 〈l,(a (m O))〉 H11' (H12 (m O)));]
-  simplify; repeat split; 
-  [1,6: apply (le_reflexive l); 
-  |2,5: apply (H12 (\fst (m 0)));
-  |3,8: apply (H12 i);
-  |4:change with (a (m O) ≤ a i);
-     apply (trans_increasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H14);
-  |7:change with (a i ≤ a (m O));
+  cases H1; cases H5; cases H7; cases (us_phi4 ?? H3 〈l,a i〉);
+  apply H15; change with (U 〈a i,l〉);
+    [apply (ous_convex_l C ? H3 ? H11 (H12 (m O)));
+    |apply (ous_convex_r C ? H3 ? H11 (H12 (m O)));]
+  [1:apply (H12 i);
+  |3: apply (le_reflexive l);
+  |4: apply (H12 i);
+  |2:change with (a (m O) ≤ a i);
+     apply (trans_increasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);
+  |5:apply (H12 i);
+  |7:apply (ge_reflexive (l : hos_carr (os_r C)));
+  |8:apply (H12 i);
+  |6:change with (a i ≤ a (m O));
      apply (trans_decreasing ? H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);]]  
 clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
 generalize in match (refl_eq nat (m p));