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