proposition: Theorem Ngreatest_div_greatest : forall p q, p>1 -> q>=1 -> q<p -> (q | p) -> q <= Ngreatest_div p.
proof: Proof. intros. apply Ngreatest_div_le_greatest; auto. destruct p. inversion H. simpl. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)