proposition: Lemma Zmod_plus_compat_rht : forall m a b : Z, (m > 0)%Z -> ((a + b) mod m)%Z = ((a + b mod m) mod m)%Z.
proof: Proof. intros m a b Hm. rewrite (Zmod_plus_compat m a b Hm). rewrite <- (Zmod_Zmod m (a + b mod m) Hm). rewrite (Zmod_plus_compat m a (b mod m) Hm). rewrite Zmod_Zmod; auto. rewrite Zmod_Zmod; auto. Qed.
imports: CoRN.model.Zmod.ZGcd