proposition: Lemma encode_bound z : (0 <= z < [M] -> 0 <= [encode n z] < [M])%Z.
proof: Proof. intros Hz. rewrite encode_correct; auto with zarith. apply Z_mod_lt; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63