proposition: Lemma encode_correct z : (0 <= z < [M] -> [encode n z] = (z * Zpower_nat wB n) mod [M])%Z.
proof: Proof. intros Hz. unfold encode; rewrite Zmod_small; auto with zarith. rewrite <-(Zmod_small _ [M]); auto with zarith. apply (eq_Tn_correct _ _ n). rewrite reduce_mult_correct. unfold r_square. rewrite !num_to_Z; auto with zarith. rewrite Zmult_mod, Zmod_mod, <-Zmult_mod, Zmult_assoc; auto with zarith. apply reduce_mult_bound_small; auto with zarith. rewrite num_to_Z; auto with zarith. unfold r_square. rewrite num_to_Z; auto with zarith. apply Z_mod_lt; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63