proposition: Lemma is_evenE : forall x, is_even x = Z.even φ (x)%uint63.
proof: Proof. intros. generalize (is_even_spec x). rewrite Z_evenE. destruct (is_even x). - symmetry. apply Z.eqb_eq. auto. - symmetry. apply Z.eqb_neq. congruence. Qed.
imports: ZArith Uint63 ZifyBool