proposition: Lemma amd_correct a b n : [amd_num a b n] = (to_Z a * [n] + to_Z b)%Z.
proof: Proof. generalize a b; clear a b; induction n as [ | c n1 Hrec]; intros a b; unfold amd_num; fold amd_num; nrom; nrom. ring. unfold amd; generalize (mulc_WW_spec a c); nrom. case (a *c c); simpl zn2z_to_Z. nrom; rewrite Hrec, to_Z_0; repeat rewrite Zmult_plus_distr_l. intros H; ring_simplify; rewrite <-H; ring. intros xh xl Hx; generalize (add_cp xl b); case (_ ?= _); intros H1; nrom; rewrite H1, Hrec; repeat rewrite Zmult_plus_distr_r; rewrite <- Hx; try ring. replace (to_Z (succ xh)) with (to_Z xh + 1)%Z; try ring. case (to_Z_bounded a); nrom; intros H1a H2a. case (to_Z_bounded c); nrom; intros H1c H2c. case (to_Z_bounded xl); nrom; intros H1xl H2xl. rewrite succ_spec, Zmod_small; nrom; auto with zarith. case (to_Z_bounded xh); nrom; intros H1xh H2xh; split; auto with zarith. assert (HH: (to_Z a * to_Z c <= (wB - 1) * (wB - 1))%Z). apply Zmult_le_compat; auto with zarith. replace ((wB - 1) * (wB - 1))%Z with (1 + wB * (wB - 2) )%Z in HH;try ring. rewrite <-Hx, Zmult_comm, Zplus_comm in HH. assert (HH1: (0 <= 1 < wB)%Z); case (to_Z_bounded 1); nrom; auto with zarith. generalize (base_lexi_order (to_Z xl) 1 (to_Z xh) (wB - 2) wB (to_Z_bounded xl) HH1). case (Zle_lt_or_eq _ _ HH); intros HH2. red in HH2; rewrite HH2; auto with zarith. rewrite HH2, Z.compare_refl; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63