proposition: Theorem Zeq_bool_opp : forall x y, Zeq_bool (Z.opp x) y = Zeq_bool x (Z.opp y).
proof: Proof. intros x y. case Zeq_bool_spec. - intros <-. apply eq_sym, Zeq_bool_true. apply eq_sym, Z.opp_involutive. - intros H. case Zeq_bool_spec. 2: easy. intros ->. contradict H. apply Z.opp_involutive. Qed.
imports: Coq(ZArith Lia Zquot)