proposition: Lemma divides_plus1 : forall a b c : nat, divides a b -> divides a c -> divides a (b + c).
proof: Proof. intros a b c (q1, H1) (q2, H2); exists (q1 + q2); rewrite H1; rewrite H2; auto with arith. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)