proposition: Lemma Zmod_div_mod n m a: 0 < n -> 0 < m -> (n | m) -> a mod n = (a mod m) mod n.
proof: Proof. Proof with auto using Z_lt_neq. intros H1 H2 (p,Hp). rewrite (Z.div_mod a m) at 1... rewrite Hp at 1. rewrite Z.mul_shuffle0, Z.add_comm, Z.mod_add... Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat