proposition: Lemma M_pos : (0 < [M])%Z.
proof: Proof. rewrite to_Z_head_tail. nrom; case (to_Z_bounded (nhead M)); nrom; intros H1a H2a. case (Zle_lt_or_eq _ _ H1a); intros H3a. assert (Hms := to_Z_pos (ntail M)). apply Z.lt_le_trans with (to_Z (nhead M) + wB * 0)%Z; auto with zarith. generalize Hmm'; rewrite mul_spec; nrom. rewrite <-H3a, Zmult_0_l, Zmod_0_l; auto with zarith. simpl; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63