proposition: Lemma decode_encode_mult p1 p2 : (0 <= p1 < [M])%Z -> (0 <= p2 < [M])%Z -> decode n (reduce_mult_num n (encode n p1) (encode n p2)) = ((p1 * p2) mod [M])%Z.
proof: Proof. intros Hp1 Hp2. rewrite <-(Zmod_small _ [M]). apply (eq_Tn_correct _ _ n). unfold decode; rewrite reduce_correct. apply (eq_Tn_correct _ _ n). rewrite reduce_mult_correct. rewrite !encode_correct by auto with zarith. rewrite <-Zmult_mod. apply f_equal2 with (f := Z.modulo). ring. reflexivity. unfold decode; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63