proposition: Theorem divide_le: forall p q, (1 < q)%nat -> divide p q -> (p <= q)%nat.
proof: Proof. intros p1 q1 H (x, H1); subst. apply Nat.le_trans with (p1 * 1)%nat; auto with arith. rewrite Nat.mul_1_r; auto with arith. apply Nat.mul_le_mono_l. destruct x; auto with arith. rewrite Nat.mul_0_r in H; auto with arith. Qed.
imports: Arith