proposition: Theorem Zeq_bool_spec : forall x y, Zeq_bool_prop x y (Zeq_bool x y).
proof: Proof. intros x y. generalize (Zeq_is_eq_bool x y). case (Zeq_bool x y) ; intros (H1, H2) ; constructor. now apply H2. intros H. specialize (H1 H). discriminate H1. Qed.
imports: Coq(ZArith Lia Zquot)