|false \Rightarrow z \neq OZ].
intros.elim z.
simplify.reflexivity.
-simplify.intros [H].
+simplify.intros (H).
discriminate H.
-simplify.intros [H].
+simplify.intros (H).
discriminate H.
qed.
theorem injective_pos: injective nat Z pos.
simplify.
intros.
-change with abs (pos x) = abs (pos y).
+change with (abs (pos x) = abs (pos y)).
apply eq_f.assumption.
qed.
theorem injective_neg: injective nat Z neg.
simplify.
intros.
-change with abs (neg x) = abs (neg y).
+change with (abs (neg x) = abs (neg y)).
apply eq_f.assumption.
qed.
\def injective_neg.
theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.
-simplify.intros [n; H].
+simplify.intros (n H).
discriminate H.
qed.
theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.
-simplify.intros [n; H].
+simplify.intros (n H).
discriminate H.
qed.
theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.
-simplify.intros [n; m; H].
+simplify.intros (n m H).
discriminate H.
qed.
elim y.
(* goal: x=pos y=OZ *)
right.intro.
- apply not_eq_OZ_pos n. symmetry. assumption.
+ apply (not_eq_OZ_pos n). symmetry. assumption.
(* goal: x=pos y=pos *)
elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
left.apply eq_f.assumption.
- right.intros [H_inj].apply H. injection H_inj. assumption.
+ right.intros (H_inj).apply H. injection H_inj. assumption.
(* goal: x=pos y=neg *)
- right.intro.apply not_eq_pos_neg n n1. assumption.
+ right.intro.apply (not_eq_pos_neg n n1). assumption.
(* goal: x=neg *)
elim y.
(* goal: x=neg y=OZ *)
right.intro.
- apply not_eq_OZ_neg n. symmetry. assumption.
+ apply (not_eq_OZ_neg n). symmetry. assumption.
(* goal: x=neg y=pos *)
- right. intro. apply not_eq_pos_neg n1 n. symmetry. assumption.
+ right. intro. apply (not_eq_pos_neg n1 n). symmetry. assumption.
(* goal: x=neg y=neg *)
elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
left.apply eq_f.assumption.