proposition: Lemma Zdiv_plus_elim : forall a b d : Z, Zdivides d a -> Zdivides d b -> ((a + b) / d)%Z = (a / d + b / d)%Z.
proof: Proof. intros a b d Ha Hb. case (Zdec d). intro Hd; rewrite Hd; case (a + b)%Z; case a; case b; simpl in |- *; auto. intro Hd. elim Ha; clear Ha; intros x Ha; rewrite <- Ha. elim Hb; clear Hb; intros y Hb; rewrite <- Hb. rewrite <- Zmult_plus_distr_l. repeat rewrite Zdiv_mult_cancel_rht; auto. Qed.
imports: CoRN.model.Zmod.ZBasics