proposition: Theorem mod_mult_comp: forall n m p, 0 < p -> mod (p * m + n) p = mod n p.
proof: Proof. intros n m p H; apply Nat.add_cancel_l with (div (p * m + n) p * p). rewrite <- div_mod_correct, div_mult_comp, Nat.mul_add_distr_r, (Nat.mul_comm p), <- Nat.add_assoc by assumption. f_equal. now apply div_mod_correct. Qed.
imports: Arith Tactic Psatz