proposition: Lemma divides_plus2 : forall a b c : nat, divides a b -> divides a (b + c) -> divides a c.
proof: Proof. intros a b c (q1, H1) (q2, H2); exists (q2 - q1). rewrite Nat.mul_sub_distr_r. rewrite <- H1. rewrite <- H2. rewrite Nat.add_comm. rewrite Nat.add_sub. reflexivity. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)