proposition: Lemma zdiv_plus_r : forall a b d : Z, ZDivides d a -> ZDivides d (a + b) -> ZDivides d b.
proof: Proof. intros. elim H. elim H0. intros. split with (x - x0)%Z. rewrite Zmult_comm. rewrite Zmult_minus_distr_r. rewrite Zmult_comm. rewrite <- H1. rewrite Zmult_comm. rewrite <- H2. rewrite Zminus_plus. reflexivity. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp