proposition: Lemma eqb_eq : forall n m, (n =? m)%sint63 = (to_Z n =? to_Z m)%Z.
proof: Proof. intros; apply Bool.eq_true_iff_eq. rewrite eqb_spec, Z.eqb_eq. split; intro H. - now subst; reflexivity. - now apply to_Z_inj in H. Qed.
imports: ZArith Sint63 ZifyBool