X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FZ%2Forders.ma;h=1f8a6d33709be06d63fdbc597df1aa7839d1d367;hb=070b44c9c2344967ca8c4531909614a0d4da2fbe;hp=c39f693085398eedf4a95a9f15898f05e6cee264;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/matita/library/Z/orders.ma b/helm/software/matita/library/Z/orders.ma
index c39f69308..1f8a6d337 100644
--- a/helm/software/matita/library/Z/orders.ma
+++ b/helm/software/matita/library/Z/orders.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Z/orders".
-
 include "Z/z.ma".
 include "nat/orders.ma".
 
@@ -36,11 +34,8 @@ definition Zle : Z \to Z \to Prop \def
     | (pos m) \Rightarrow True
     | (neg m) \Rightarrow m \leq n ]].
 
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/Z/orders/Zle.con x y).
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'neither less nor equal to'" 'nleq x y =
-  (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zle.con x y)).
+interpretation "integer 'less or equal to'" 'leq x y = (Zle x y).
+interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
 
 definition Zlt : Z \to Z \to Prop \def
 \lambda x,y:Z.
@@ -61,14 +56,11 @@ definition Zlt : Z \to Z \to Prop \def
     | (pos m) \Rightarrow True
     | (neg m) \Rightarrow m<n ]].
     
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y).
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'not less than'" 'nless x y =
-  (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zlt.con x y)).
+interpretation "integer 'less than'" 'lt x y = (Zlt x y).
+interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
 
 theorem irreflexive_Zlt: irreflexive Z Zlt.
-change with (\forall x:Z. x < x \to False).
+unfold irreflexive.unfold Not.
 intro.elim x.exact H.
 cut (neg n < neg n \to False).
 apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
@@ -76,6 +68,121 @@ cut (pos n < pos n \to False).
 apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
 qed.
 
+(* transitivity *)
+theorem transitive_Zle : transitive Z Zle.
+unfold transitive.
+intros 3.
+elim x 0
+[ (* x = OZ *)
+  elim y 0
+  [ intros. assumption 
+  | intro.
+    elim z
+    [ simplify. apply I 
+    | simplify. apply I
+    | simplify. simplify in H1. assumption
+    ]
+  | intro.
+    elim z
+    [ simplify. apply I
+    | simplify. apply I
+    | simplify. simplify in H. assumption
+    ]
+  ]
+| (* x = (pos n) *)
+  intro.
+  elim y 0
+  [ intros. apply False_ind. apply H
+  | intros 2. 
+    elim z 0
+    [ simplify. intro. assumption
+    | intro. generalize in match H. simplify. apply trans_le 
+    | intro. simplify. intro. assumption
+    ]
+  | intros 2. apply False_ind. apply H
+  ]
+| (* x = (neg n) *)
+  intro.
+  elim y 0
+  [ elim z 0
+    [ simplify. intros. assumption
+    | intro. simplify. intros. assumption
+    | intro. simplify. intros. apply False_ind. apply H1
+    ]
+  | intros 2.
+    elim z
+    [ apply False_ind. apply H1 
+    | simplify. apply I
+    | apply False_ind. apply H1
+    ]
+  | intros 2.
+    elim z 0
+    [ simplify. intro. assumption
+    | intro. simplify. intro. assumption
+    | intros. simplify. simplify in H. simplify in H1. 
+      generalize in match H. generalize in match H1. apply trans_le
+    ]
+  ]
+]
+qed.
+
+variant trans_Zle: transitive Z Zle
+\def transitive_Zle.
+
+theorem transitive_Zlt: transitive Z Zlt.
+unfold.
+intros 3.
+elim x 0
+[ (* x = OZ *)
+  elim y 0
+  [ intros. apply False_ind. apply H 
+  | intro.
+    elim z
+    [ simplify. apply H1 
+    | simplify. apply I
+    | simplify. apply H1
+    ]
+  | intros 2. apply False_ind. apply H
+  ]
+| (* x = (pos n) *)
+  intro.
+  elim y 0
+  [ intros. apply False_ind. apply H
+  | intros 2. 
+    elim z 0
+    [ simplify. intro. assumption
+    | intro. generalize in match H. simplify. apply trans_lt 
+    | intro. simplify. intro. assumption
+    ]
+  | intros 2. apply False_ind. apply H
+  ]
+| (* x = (neg n) *)
+  intro.
+  elim y 0
+  [ elim z 0
+    [ intros. simplify. apply I
+    | intro. simplify. intros. assumption
+    | intro. simplify. intros. apply False_ind. apply H1
+    ]
+  | intros 2.
+    elim z
+    [ apply False_ind. apply H1 
+    | simplify. apply I
+    | apply False_ind. apply H1
+    ]
+  | intros 2.
+    elim z 0
+    [ simplify. intro. assumption
+    | intro. simplify. intro. assumption
+    | intros. simplify. simplify in H. simplify in H1. 
+      generalize in match H. generalize in match H1. apply trans_lt
+    ]
+  ]
+]
+qed.
+
+variant trans_Zlt: transitive Z Zlt
+\def transitive_Zlt.
 theorem irrefl_Zlt: irreflexive Z Zlt
 \def irreflexive_Zlt.