proposition: Theorem divides_le : forall a b : nat, b <> 0 -> divides a b -> a <= b.
proof: Proof. intros a b; case b. intros H'; case H'; auto. intros n H (q1, H1). generalize H; rewrite H1; case q1; simpl in |- *; auto with arith. intros H2; case H2; auto. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)