proposition: Lemma shift_correct t : [shift_num t] = ([t] / wB)%Z.
proof: Proof. destruct t as [ | a t]; unfold shift_num; nrom. rewrite Zdiv_0_l; auto. case (to_Z_bounded a); nrom; intros H1a H2a. rewrite Zmult_comm, Z_div_plus_full; auto with zarith. rewrite Zdiv_small; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63