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.