proposition: Theorem Ngreatest_div_lt_p : forall n, n > 1 -> Ngreatest_div n < n.
proof: Proof. intros. destruct n. inversion H. destruct n. inversion H. inversion H1. unfold lt. apply le_n_S. unfold Ngreatest_div. replace (pred(S(S n))) with (S n). apply Ngreatest_div_le_le. auto with arith. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)