proposition: Lemma eq_Tn_correct a b n : ((a * Zpower_nat wB n) mod [M] = (b * Zpower_nat wB n) mod [M] -> a mod [M] = b mod [M])%Z.
proof: Proof. intros H. assert (HH: ((a - b) mod [M] = 0)%Z). rewrite <- (Zmult_1_r (a - b)), Zmult_mod, <- (Tn_correct n), <- Zmult_mod, (Zmult_comm [T n]), Zmult_assoc, Zmult_minus_distr_r, Zmult_mod, Zminus_mod, H, <- Zminus_mod, <- Zmult_mod, Zminus_diag, Zmult_0_l, Zmod_0_l; auto. replace a with (b + (a - b))%Z; try ring. rewrite Zplus_mod, HH, Zplus_0_r, Zmod_mod; auto. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63