(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.
+change with (\forall x:Z. x < x \to False).
intro.elim x.exact H.
-cut neg n < neg n \to False.
-apply Hcut.apply H.simplify.apply not_le_Sn_n.
-cut pos n < pos n \to False.
-apply Hcut.apply H.simplify.apply not_le_Sn_n.
+cut (neg n < neg n \to False).
+apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
+cut (pos n < pos n \to False).
+apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
qed.
theorem irrefl_Zlt: irreflexive Z Zlt
intros 2.
elim x.
(* goal: x=OZ *)
- cut OZ < y \to Zsucc OZ \leq y.
+ cut (OZ < y \to Zsucc OZ \leq y).
apply Hcut. assumption.
simplify.elim y.
simplify.exact H1.
(* goal: x=pos *)
exact H.
(* goal: x=neg *)
- cut neg n < y \to Zsucc (neg n) \leq y.
+ 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.
+ 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.
+ 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.
+ simplify.apply (le_S_S_to_le n2 n1 H3).
qed.