proposition: Theorem Nprime_greatest_div_1 : forall p, Nprime p -> Ngreatest_div p=1.
proof: Proof. intros. apply Nprime_greatest_div_le_1. destruct H. inversion H; auto with arith. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)