proposition: Lemma is_zeroE : forall n : int, is_zero n = (to_Z n =? 0)%Z.
proof: Proof. intro n; apply Bool.eq_true_iff_eq. rewrite is_zero_spec, Z.eqb_eq; split. - now intro eqn0; rewrite eqn0. - now change 0%Z with (to_Z 0); apply to_Z_inj. Qed.
imports: ZArith Sint63 ZifyBool