proposition: Lemma not_lt_div : forall a b : nat, 0 < b -> b < a -> ~ divides a b.
proof: Proof. intros a b H'1 H'2; red in |- *; intros H'3; Contradict H'2; auto with arith. apply Nat.le_ngt; apply divides_le; auto. apply sym_not_eq; auto with arith. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)