proposition: Lemma decode_encode p : (0 <= p < [M])%Z -> decode n (encode n p) = p.
proof: Proof. intros Hp. unfold decode, encode. assert (F1 : (0 <= [Z_to_num (p mod [M])] < [M])%Z). rewrite num_to_Z; auto with zarith. rewrite Zmod_small; auto with zarith. case (Z.mod_pos_bound p [M]); auto with zarith. assert (F2: ([Z_to_num (p mod [M])] < Zpower_nat wB n)%Z). apply (Z.lt_trans _ [M]); auto with zarith. assert (F3: ([r_square n] < [M])%Z). case (r_square_lt n); auto. generalize (reduce_mult_bound _ _ _ F2 F3); intros F4. rewrite <-(Zmod_small p [M]); auto with zarith. rewrite <-(Zmod_small _ [M]). apply (eq_Tn_correct _ _ n). rewrite reduce_correct. apply (eq_Tn_correct _ _ n). rewrite reduce_mult_correct. unfold r_square. rewrite !num_to_Z; auto with zarith. rewrite Zmod_mod, <-Zmult_mod, Zmult_assoc; auto. case (Z.mod_pos_bound (Zpower_nat wB n * Zpower_nat wB n) [M]); auto with zarith. case (Z.mod_pos_bound (p mod [M]) [M]); auto with zarith. case (Z.mod_pos_bound p [M]); auto with zarith. intros; apply reduce_bound_small. rewrite Zmod_mod; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63