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