proposition: Lemma zeq_bool_eq : forall x y : Z, x = y <-> Zeq_bool x y = true.
proof: Proof. intros. elim (Zcompare_Eq_iff_eq x y). intros. unfold Zeq_bool in |- *. split. intro. rewrite H0. reflexivity. assumption. intro. apply H. generalize H1. elim (x ?= y)%Z. intro. reflexivity. intro. discriminate H2. intro. discriminate H2. Qed.
imports: Arith ZArith EqNat