proposition: Lemma Zdivides_plus_elim : forall a b c : Z, Zdivides a b -> Zdivides a c -> Zdivides a (b + c).
proof: Proof. intros a b c H1 H2. unfold Zdivides in H1; elim H1; intros q1 H1_. unfold Zdivides in H2; elim H2; intros q2 H2_. exists (q1 + q2)%Z. rewrite Zmult_plus_distr_l. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZBasics