(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/orders".
-
include "Z/z.ma".
include "nat/orders.ma".
| (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.
| (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.
unfold irreflexive.unfold Not.
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.