proposition: Theorem divides_trans : forall a b c : nat, divides a b -> divides b c -> divides a c.
proof: Proof. intros a b c (q1, H1) (q2, H2); exists (q1 * q2); rewrite H2; rewrite H1; ring. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)