proposition: Lemma decode_encode_sub p1 p2 : (0 <= p1 < [M])%Z -> (0 <= p2 < [M])%Z -> decode n (sub_mod M (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. rewrite sub_mod_correct; auto with zarith. rewrite !encode_correct; auto with zarith. rewrite <-Zminus_mod, Zmod_mod, Zmult_minus_distr_r; auto with zarith. unfold decode; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63