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