proposition: Lemma Ngreatest_div_le_div : forall p n, p>1 -> (Ngreatest_div_le n p | p).
proof: Proof. induction n. intros. compute. apply Ndiv_1. intros. simpl. destruct n. apply Ndiv_1. assert(Ndiv_algo (S(S n)) p=true -> (S(S n)|p)). intros. apply Ndiv_algo_complete. auto with arith. auto. destruct (Ndiv_algo (S(S n)) p). apply H0. auto. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)