proposition: Theorem Zeq_bool_false : forall x y, x <> y -> Zeq_bool x y = false.
proof: Proof. intros x y. generalize (proj2 (Zeq_is_eq_bool x y)). case Zeq_bool. intros He Hn. elim Hn. now apply He. now intros _ _. Qed.
imports: Coq(ZArith Lia Zquot)