set "baseuri" "cic:/matita/Z/orders".
include "Z/z.ma".
+include "nat/orders.ma".
definition Zle : Z \to Z \to Prop \def
\lambda x,y:Z.
theorem irrefl_Zlt: irreflexive Z Zlt
\def irreflexive_Zlt.
-definition Z_compare : Z \to Z \to compare \def
-\lambda x,y:Z.
- match x with
- [ OZ \Rightarrow
- match y with
- [ OZ \Rightarrow EQ
- | (pos m) \Rightarrow LT
- | (neg m) \Rightarrow GT ]
- | (pos n) \Rightarrow
- match y with
- [ OZ \Rightarrow GT
- | (pos m) \Rightarrow (nat_compare n m)
- | (neg m) \Rightarrow GT]
- | (neg n) \Rightarrow
- match y with
- [ OZ \Rightarrow LT
- | (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.
+\forall n,m:nat. neg n < neg m \to 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.
+theorem lt_to_Zlt_neg_neg: \forall n,m:nat.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.
+\forall n,m:nat. pos n < pos m \to 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.
+theorem lt_to_Zlt_pos_pos: \forall n,m:nat.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 x < y
-| EQ \Rightarrow x=y
-| GT \Rightarrow y < x].
-intros.
-elim x. elim y.
-simplify.apply refl_eq.
-simplify.exact I.
-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 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 neg n = neg n1
-| GT \Rightarrow (le (S n) n1)].
-apply Hcut. apply nat_compare_to_Prop.
-elim (nat_compare n1 n).
-simplify.exact H.
-simplify.exact H.
-simplify.apply eq_f.apply sym_eq.exact H.
-simplify.exact I.
-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 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 pos n = pos n1
-| GT \Rightarrow (le (S n1) n)].
-apply Hcut. apply nat_compare_to_Prop.
-elim (nat_compare n n1).
-simplify.exact H.
-simplify.exact H.
-simplify.apply eq_f.exact H.
-qed.
-
theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
intros 2.elim x.
cut OZ < y \to Zsucc OZ \leq y.