proposition: Lemma Zeq_spec : forall (x y:Z), if Zeq_bool x y then x = y else x<>y.
proof: Proof. unfold Zeq_bool; intros. case_eq (x ?= y)%Z. - apply Z.compare_eq_iff. - intro. rewrite Z.compare_lt_iff in H. auto with zarith. - intro. rewrite Z.compare_gt_iff in H. auto with zarith. Qed.
imports: Coq(ZArith)