proposition: Lemma Zmod_Zmod : forall m a : Z, (m > 0)%Z -> ((a mod m) mod m)%Z = (a mod m)%Z.
proof: Proof. intros m a Hm. apply (Zdiv_remainder_unique (a mod m) m (a mod m / m) ((a mod m) mod m) 0 (a mod m)). rewrite Zmult_comm. apply Z_div_mod_eq_full. apply Z_mod_lt; auto. auto with zarith. apply Z_mod_lt; auto. Qed.
imports: CoRN.model.Zmod.ZGcd