match eqZb x y with
[ true \Rightarrow x=y
| false \Rightarrow \lnot x=y].
-intros.elim x.
-elim y.
-simplify.reflexivity.
-simplify.apply not_eq_OZ_neg.
-simplify.apply not_eq_OZ_pos.
-elim y.
-simplify.intro.apply not_eq_OZ_neg n ?.apply sym_eq.assumption.
-simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
-intro.simplify.intro.apply H.apply inj_neg.assumption.
-simplify.intro.apply not_eq_pos_neg n1 n ?.apply sym_eq.assumption.
-elim y.
-simplify.intro.apply not_eq_OZ_pos n ?.apply sym_eq.assumption.
-simplify.apply not_eq_pos_neg.
-simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
-intro.simplify.intro.apply H.apply inj_pos.assumption.
+intros.
+elim x.
+ elim y.
+ simplify.reflexivity.
+ 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.apply eqb_elim.
+ intro.simplify.apply eq_f.assumption.
+ intro.simplify.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.apply eqb_elim.
+ intro.simplify.apply eq_f.assumption.
+ intro.simplify.intro.apply H.apply inj_neg.assumption.
qed.
theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
| EQ \Rightarrow x=y
| GT \Rightarrow y < x].
intros.
-elim x. elim y.
-simplify.apply refl_eq.
-simplify.exact I.
-simplify.exact I.
-elim y. simplify.exact I.
-simplify.
-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].
-apply Hcut. apply nat_compare_to_Prop.
-elim (nat_compare n1 n).
-simplify.exact H.
-simplify.exact H.
-simplify.apply eq_f.apply sym_eq.exact H.
-simplify.exact I.
-elim y.simplify.exact I.
-simplify.exact I.
-simplify.
-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].
-apply Hcut. apply nat_compare_to_Prop.
-elim (nat_compare n n1).
-simplify.exact H.
-simplify.exact H.
-simplify.apply eq_f.exact H.
+elim x.
+ elim y.
+ simplify.apply refl_eq.
+ simplify.exact I.
+ simplify.exact I.
+ elim y.
+ simplify.exact I.
+ simplify.
+ 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].
+ apply Hcut.apply nat_compare_to_Prop.
+ elim (nat_compare n n1).
+ simplify.exact H.
+ simplify.apply eq_f.exact H.
+ simplify.exact H.
+ simplify.exact I.
+ elim y.
+ simplify.exact I.
+ simplify.exact I.
+ simplify.
+ 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].
+ apply Hcut. apply nat_compare_to_Prop.
+ elim (nat_compare n1 n).
+ simplify.exact H.
+ simplify.apply eq_f.apply sym_eq.exact H.
+ simplify.exact H.
qed.