proposition: Theorem Z_eq_bool_correct : forall p q : Z, match Z_eq_bool p q with | true => p = q | false => p <> q end.
proof: Proof. intros p q. unfold Z_eq_bool. now case Z.eqb_spec. Qed.
imports: Reals ZArith List PeanoNat Psatz