proposition: Lemma divides_div : forall x y : nat, 0 < y -> divides y x -> exists q : _, is_div x y q 0.
proof: Proof. intros x y H'1 (q, H'2); exists q; split; try rewrite H'2; auto with arith. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)