proposition: Lemma sub_mod_correct p m n : (0 <= [m] < [p] -> 0 <= [n] < [p] -> [sub_mod p m n] = ([m] - [n]) mod [p])%Z.
proof: Proof. intros H1 H2; unfold sub_mod. case cp_spec; intros H3. rewrite H3, Zminus_diag, Zmod_0_l, sub_correct, H3; auto with zarith. rewrite sub_correct; rewrite add_correct; auto with zarith. rewrite <-(fun x y => (Zmod_small (x - y) [p])); auto with zarith. rewrite Zminus_mod, Zplus_mod, Z_mod_same_full, Zplus_0_l, Zmod_mod, <- Zminus_mod; auto. rewrite Zmod_small, sub_correct; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63