proposition: Lemma num_to_Z z : (0 <= z)%Z -> [Z_to_num z] = z.
proof: Proof. destruct z as [|p|p]; intros Hp. auto with zarith. apply positive_to_Z. contradict Hp; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63