proposition: Lemma div_plus_r : forall a b d : nat, Divides d a -> Divides d (a + b) -> Divides d b.
proof: Proof. intros. elim H. elim H0. intros. split with (x - x0). rewrite mult_comm. rewrite mult_minus_distr_r. rewrite mult_comm. rewrite <- H1. rewrite mult_comm. rewrite <- H2. rewrite minus_plus. reflexivity. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp