| (pos n) \Rightarrow
match y with
[ OZ \Rightarrow False
- | (pos m) \Rightarrow (le n m)
+ | (pos m) \Rightarrow n \leq m
| (neg m) \Rightarrow False ]
| (neg n) \Rightarrow
match y with
[ OZ \Rightarrow True
| (pos m) \Rightarrow True
- | (neg m) \Rightarrow (le m n) ]].
+ | (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: 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.
| (pos n) \Rightarrow
match y with
[ OZ \Rightarrow False
- | (pos m) \Rightarrow (lt n m)
+ | (pos m) \Rightarrow n<m
| (neg m) \Rightarrow False ]
| (neg n) \Rightarrow
match y with
[ OZ \Rightarrow True
| (pos m) \Rightarrow True
- | (neg m) \Rightarrow (lt m n) ]].
+ | (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: 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. x < x \to False.
| (pos m) \Rightarrow LT
| (neg m) \Rightarrow nat_compare m n ]].
+(*CSC: qui uso lt perche' ho due istanze diverse di < *)
theorem Zlt_neg_neg_to_lt:
\forall n,m:nat. neg n < neg m \to lt m n.
intros.apply H.
qed.
+(*CSC: qui uso lt perche' ho due istanze diverse di < *)
theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to neg n < neg m.
intros.
simplify.apply H.
qed.
+(*CSC: qui uso lt perche' ho due istanze diverse di < *)
theorem Zlt_pos_pos_to_lt:
\forall n,m:nat. pos n < pos m \to lt n m.
intros.apply H.
qed.
+(*CSC: qui uso lt perche' ho due istanze diverse di < *)
theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to pos n < pos m.
intros.
simplify.apply H.
simplify.exact I.
elim y. simplify.exact I.
simplify.
+(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
+ per via delle coercions! *)
cut match (nat_compare n1 n) with
-[ LT \Rightarrow (lt n1 n)
-| EQ \Rightarrow (eq nat n1 n)
-| GT \Rightarrow (lt n n1)] \to
+[ LT \Rightarrow n1<n
+| EQ \Rightarrow n1=n
+| GT \Rightarrow n<n1] \to
match (nat_compare n1 n) with
[ LT \Rightarrow (le (S n1) n)
-| EQ \Rightarrow (eq Z (neg n) (neg n1))
+| EQ \Rightarrow neg n = neg n1
| GT \Rightarrow (le (S n) n1)].
apply Hcut. apply nat_compare_to_Prop.
elim (nat_compare n1 n).
elim y.simplify.exact I.
simplify.exact I.
simplify.
+(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
+ per via delle coercions! *)
cut match (nat_compare n n1) with
-[ LT \Rightarrow (lt n n1)
-| EQ \Rightarrow (eq nat n n1)
-| GT \Rightarrow (lt n1 n)] \to
+[ LT \Rightarrow n<n1
+| EQ \Rightarrow n=n1
+| GT \Rightarrow n1<n] \to
match (nat_compare n n1) with
[ LT \Rightarrow (le (S n) n1)
-| EQ \Rightarrow (eq Z (pos n) (pos n1))
+| EQ \Rightarrow pos n = pos n1
| GT \Rightarrow (le (S n1) n)].
apply Hcut. apply nat_compare_to_Prop.
elim (nat_compare n n1).