(*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)).
definition Zlt : Z \to Z \to Prop \def
\lambda x,y:Z.
(*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)).
theorem irreflexive_Zlt: irreflexive Z Zlt.
change with \forall x:Z. x < x \to False.
theorem irrefl_Zlt: irreflexive Z Zlt
\def irreflexive_Zlt.
-(*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 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.
-apply Hcut. assumption.simplify.elim y.
-simplify.exact H1.
-simplify.exact H1.
-simplify.apply le_O_n.
-cut neg n < y \to Zsucc (neg n) \leq y.
-apply Hcut. assumption.elim n.
-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 neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
-apply Hcut. assumption.simplify.
-elim y.
-simplify.exact I.
-simplify.apply le_S_S_to_le n2 n1 H3.
-simplify.exact I.
-exact H.
+intros 2.
+elim x.
+(* goal: x=OZ *)
+ cut OZ < y \to Zsucc OZ \leq y.
+ apply Hcut. assumption.
+ simplify.elim y.
+ simplify.exact H1.
+ simplify.apply le_O_n.
+ simplify.exact H1.
+(* goal: x=pos *)
+ exact H.
+(* goal: x=neg *)
+ cut neg n < y \to Zsucc (neg n) \leq y.
+ apply Hcut. assumption.
+ elim n.
+ cut neg O < y \to Zsucc (neg O) \leq y.
+ apply Hcut. assumption.
+ simplify.elim y.
+ simplify.exact I.
+ simplify.exact I.
+ simplify.apply not_le_Sn_O n1 H2.
+ cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
+ apply Hcut. assumption.simplify.
+ elim y.
+ simplify.exact I.
+ simplify.exact I.
+ simplify.apply le_S_S_to_le n2 n1 H3.
qed.