proposition: Theorem Ngreatest_div_le_greatest : forall n p q, p>1 -> q>=1 -> q<p -> q<=n -> (q | p) -> q <= Ngreatest_div_le n p.
proof: Proof. intros. replace q with (Ngreatest_div_le q p). apply Ngreatest_div_le_monotone. auto. destruct q. inversion H0. simpl. destruct q. auto. apply Ndiv_algo_correct in H3. rewrite H3. auto. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)