proposition: Lemma zeq_bool_neq : forall x y : Z, x <> y <-> Zeq_bool x y = false.
proof: Proof. intros. elim (Zcompare_Eq_iff_eq x y). intros. unfold Zeq_bool in |- *. split. generalize H0. generalize H. elim (x ?= y)%Z. intros. elim H3. apply H1. reflexivity. intros. reflexivity. intros. reflexivity. intros. generalize H1. generalize H0. elim (x ?= y)%Z. intros. discriminate H3. intros. intro. cut (Datatypes.Lt = Datatypes.Eq). discriminate. apply H2. assumption. intros. intro. cut (Datatypes.Gt = Datatypes.Eq). discriminate. apply H2. assumption. Qed.
imports: Arith ZArith EqNat