proposition: Theorem Ngreatest_div_1_prime : forall p, p > 1 -> Ngreatest_div p = 1 -> Nprime p.
proof: Proof. intro. destruct p. intros. inversion H. destruct p. intros. inversion H. inversion H2. intros. split. auto. intros. intro. apply Ngreatest_div_greatest in H2. rewrite H0 in H2. destruct H1. assert(1<1). eapply Nat.le_trans. eapply H1. auto. inversion H4. inversion H6. auto with arith. destruct H1. auto with arith. destruct H1. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)