proposition: Lemma Z_of_nat_eqb_iff n m : (n =? m)%nat = (Z.of_nat n =? Z.of_nat m).
proof: Proof. rewrite Nat.eqb_compare. rewrite Z.eqb_compare. rewrite Nat2Z.inj_compare. reflexivity. Qed.
imports: Bool ZArith Zify ZifyClasses ZifyInst