proposition: Lemma reduce_aux_step a t : ((to_Z a + wB * [t] + to_Z (a * m') * [M]) / wB * wB = to_Z a + wB * [t] + to_Z (a * m') * [M])%Z.
proof: Proof. case (to_Z_bounded a); nrom; intros H1a H2a. rewrite (to_Z_head_tail M); nrom. set (m := nhead M); set (ms := ntail M). replace (to_Z a + wB * [t] + to_Z (a * m') * (to_Z m + wB * [ms]))%Z with ((to_Z a + to_Z (a * m') * to_Z m) + ([t] + to_Z (a * m') * [ms]) * wB)%Z; try ring. rewrite Z_div_plus_full; auto with zarith. set (v := (to_Z a + to_Z (a * m') * to_Z m)%Z). assert (HH: (v / wB * wB = v)%Z). rewrite (Z_div_mod_eq_full v wB); auto with zarith. rewrite (Zmult_comm wB), Z_div_plus_full_l; auto with zarith. assert (HH: (v mod wB = 0)%Z); auto with zarith. unfold v; rewrite mul_spec; nrom. rewrite Zplus_mod, Zmult_mod, Zmod_mod, <- Zmult_mod, <- Zmult_assoc, Zmult_mod. unfold m. generalize Hmm'; rewrite mul_spec; nrom; intros HH1; rewrite (Zmult_comm (to_Z m')), HH1. rewrite (Zmult_mod (to_Z a mod wB)), Zmod_mod, <- Zmult_mod, <- Zplus_mod. replace (to_Z a + to_Z a * (wB - 1))%Z with (to_Z a * wB)%Z; try ring. rewrite Z_mod_mult; auto. rewrite Zmult_plus_distr_l, HH, Zdiv_0_l, Zmult_0_l, <-HH, Zmult_comm, <- Z_div_mod_eq_full; auto with zarith. rewrite Zmult_plus_distr_l, HH; unfold v. nrom; ring. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63