simplify.apply not_eq_OZ_pos.
simplify.apply not_eq_OZ_neg.
elim y.
- simplify.intro.apply not_eq_OZ_pos n.apply sym_eq.assumption.
+ simplify.unfold Not.intro.apply (not_eq_OZ_pos n).apply sym_eq.assumption.
simplify.apply eqb_elim.
intro.simplify.apply eq_f.assumption.
- intro.simplify.intro.apply H.apply inj_pos.assumption.
+ intro.simplify.unfold Not.intro.apply H.apply inj_pos.assumption.
simplify.apply not_eq_pos_neg.
elim y.
- simplify.intro.apply not_eq_OZ_neg n.apply sym_eq.assumption.
- simplify.intro.apply not_eq_pos_neg n1 n.apply sym_eq.assumption.
+ simplify.unfold Not.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption.
+ simplify.unfold Not.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption.
simplify.apply eqb_elim.
intro.simplify.apply eq_f.assumption.
- intro.simplify.intro.apply H.apply inj_neg.assumption.
+ intro.simplify.unfold Not.intro.apply H.apply inj_neg.assumption.
qed.
theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
(x=y \to (P true)) \to (x \neq y \to (P false)) \to P (eqZb x y).
intros.
cut
-match (eqZb x y) with
+(match (eqZb x y) with
[ true \Rightarrow x=y
-| false \Rightarrow x \neq y] \to P (eqZb x y).
+| false \Rightarrow x \neq y] \to P (eqZb x y)).
apply Hcut.
apply eqZb_to_Prop.
elim (eqZb).
-apply H H2.
-apply H1 H2.
+apply (H H2).
+apply (H1 H2).
qed.
definition Z_compare : Z \to Z \to compare \def
elim y.
simplify.exact I.
simplify.
- cut match (nat_compare n n1) with
+ 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 (S n) \leq n1
| EQ \Rightarrow pos n = pos n1
- | GT \Rightarrow (S n1) \leq n].
+ | GT \Rightarrow (S n1) \leq n]).
apply Hcut.apply nat_compare_to_Prop.
elim (nat_compare n n1).
simplify.exact H.
simplify.exact I.
simplify.exact I.
simplify.
- cut match (nat_compare n1 n) with
+ 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 (S n1) \leq n
| EQ \Rightarrow neg n = neg n1
- | GT \Rightarrow (S n) \leq n1].
+ | GT \Rightarrow (S n) \leq n1]).
apply Hcut. apply nat_compare_to_Prop.
elim (nat_compare n1 n).
simplify.exact H.