proposition: Lemma divides_dec' : forall x y : nat, {(exists q : _, is_div x y q 0)} + {~ (exists q : _, is_div x y q 0)}.
proof: Proof. intros x y; case y; auto. right; red in |- *; intros (q, (H1, H2)); Contradict H1; auto with arith. intros y'; case (eucl_dev (S y') (Nat.lt_0_succ y') x). intros q r; case r; auto. intros H' H'0; left; exists q; split; try rewrite H'0; auto with arith. intros n H' H'0; right; red in |- *; intros (q1, (H1, H2)); absurd (0 = S n); auto with arith. apply div_unic_r with (a := x) (b := S y') (q1 := q1) (q2 := q); split; auto with arith. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)