proposition: Lemma ltb_lt : forall n m, (n <? m)%uint63 = (φ (n)%uint63 <? φ (m)%uint63)%Z.
proof: Proof. intros. apply Bool.eq_true_iff_eq. rewrite ltb_spec. rewrite <- Z.ltb_lt. apply iff_refl. Qed.
imports: ZArith Uint63 ZifyBool