More notation (up to where the open bugs allow me to put it without adding

[helm.git] / helm / matita / library / Z / orders.ma

diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
index 1a2d65a4f05e6dc8c85654ca7c203fab1e72e41f..60c727cebe9ff7967f2971b1916eb34f8c24cd4b 100644 (file)
--- a/helm/matita/library/Z/orders.ma
+++ b/helm/matita/library/Z/orders.ma
@@ -35,6 +35,10 @@ definition Zle : Z \to Z \to Prop \def
     | (pos m) \Rightarrow True
     | (neg m) \Rightarrow (le m 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: this alias must disappear: there is a bug in the generation of the .moos *)
+alias symbol "leq" (instance 0) = "integer 'less or equal to'".
 
 definition Zlt : Z \to Z \to Prop \def
 \lambda x,y:Z.
@@ -55,12 +59,17 @@ definition Zlt : Z \to Z \to Prop \def
     | (pos m) \Rightarrow True
     | (neg m) \Rightarrow (lt 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: this alias must disappear: there is a bug in the generation of the .moos *)
+alias symbol "lt" (instance 0) = "integer 'less than'".
+
 theorem irreflexive_Zlt: irreflexive Z Zlt.
-change with \forall x:Z. Zlt x x \to False.
+change with \forall x:Z. x < x \to False.
 intro.elim x.exact H.
-cut (Zlt (neg n) (neg n)) \to False.
+cut neg n < neg n \to False.
 apply Hcut.apply H.simplify.apply not_le_Sn_n.
-cut (Zlt (pos n) (pos n)) \to False.
+cut pos n < pos n \to False.
 apply Hcut.apply H.simplify.apply not_le_Sn_n.
 qed.
 
@@ -87,30 +96,30 @@ definition Z_compare : Z \to Z \to compare \def
     | (neg m) \Rightarrow nat_compare m n ]].
 
 theorem Zlt_neg_neg_to_lt: 
-\forall n,m:nat. Zlt (neg n) (neg m) \to lt m n.
+\forall n,m:nat. neg n < neg m \to lt m n.
 intros.apply H.
 qed.
 
-theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to Zlt (neg n) (neg m). 
+theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to neg n < neg m. 
 intros.
 simplify.apply H.
 qed.
 
 theorem Zlt_pos_pos_to_lt: 
-\forall n,m:nat. Zlt (pos n) (pos m) \to lt n m.
+\forall n,m:nat. pos n < pos m \to lt n m.
 intros.apply H.
 qed.
 
-theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to Zlt (pos n) (pos m). 
+theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to pos n < pos m. 
 intros.
 simplify.apply H.
 qed.
 
 theorem Z_compare_to_Prop : 
 \forall x,y:Z. match (Z_compare x y) with
-[ LT \Rightarrow (Zlt x y)
-| EQ \Rightarrow (eq Z x y)
-| GT \Rightarrow (Zlt y x)]. 
+[ LT \Rightarrow x < y
+| EQ \Rightarrow x=y
+| GT \Rightarrow y < x]. 
 intros.
 elim x. elim y.
 simplify.apply refl_eq.
@@ -150,20 +159,20 @@ simplify.exact H.
 simplify.apply eq_f.exact H.
 qed.
 
-theorem Zlt_to_Zle: \forall x,y:Z. Zlt x y \to Zle (Zsucc x) y.
+theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
 intros 2.elim x.
-cut (Zlt OZ y) \to (Zle (Zsucc OZ) y).
+cut OZ < y \to Zsucc OZ \leq y.
 apply Hcut. assumption.simplify.elim y.
 simplify.exact H1.
 simplify.exact H1.
 simplify.apply le_O_n.
-cut (Zlt (neg n) y) \to (Zle (Zsucc (neg n)) y).
+cut neg n < y \to Zsucc (neg n) \leq y.
 apply Hcut. assumption.elim n.
-cut (Zlt (neg O) y) \to (Zle (Zsucc (neg O)) y).
+cut neg O < y \to Zsucc (neg O) \leq y.
 apply Hcut. assumption.simplify.elim y.
 simplify.exact I.simplify.apply not_le_Sn_O n1 H2.
 simplify.exact I.
-cut (Zlt (neg (S n1)) y) \to (Zle (Zsucc (neg (S n1))) y).
+cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
 apply Hcut. assumption.simplify.
 elim y.
 simplify.exact I.