proposition: Lemma divides_dec : forall x y : nat, {divides x y} + {~ divides x y}.
proof: Proof. intros x y; case x; case y; auto. left; exists 0; auto. intros n; right; red in |- *; intros (q, H'). rewrite (Nat.mul_comm q 0) in H'; discriminate. intros n; left; exists 0; auto. intros x' y'; case (divides_dec' (S x') (S y')); auto. intros H'; left; apply div_divides; auto. intros H'; right; red in |- *; intros (q1, H1); case H'; auto. exists q1; split; try rewrite H1; auto with arith. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)