proposition: Lemma Tn_correct n : ([T n] * (Zpower_nat wB n) mod [M] = 1 mod[M])%Z.
proof: Proof. unfold T; rewrite reduce_correct; nrom; nrom. rewrite Zmult_0_r, Zplus_0_r; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63