proposition: Lemma Zmod_div_mod: forall n m a, 0 < n -> 0 < m -> (n | m) -> a mod n = (a mod m) mod n.
proof: Proof. intros n m a H1 H2 H3. pattern a at 1; rewrite (Z_div_mod_eq_full a m). case H3; intros q Hq; pattern m at 1; rewrite Hq. rewrite (Zmult_comm q). rewrite Zplus_mod; auto. rewrite <- Zmult_assoc; rewrite Zmult_mod; auto. rewrite Z_mod_same; try rewrite Zmult_0_l; auto with zarith. rewrite (Zmod_small 0); auto with zarith. rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith. Qed.
imports: ZArith Znumtheory