proposition: Lemma Zmodeq_plus_compat : forall a b c d : Z, Zmodeq a b -> Zmodeq c d -> Zmodeq (a + c) (b + d).
proof: Proof. intros a b c d. unfold Zmodeq in |- *. unfold Zdivides in |- *. intros Hab Hcd. elim Hab. intros q1 H1. elim Hcd. intros q2 H2. exists (q1 + q2)%Z. rewrite Zmult_plus_distr_l. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZGcd