proposition: Lemma Nleast_div_ge_div : forall p n, p>1 -> n < p -> (Nleast_div_ge n p | p).
proof: Proof. induction n. intros. compute. apply Ndiv_n_n. intros. simpl. assert (Ndiv_algo (p-S n) p=true -> (p-S n|p)). apply Ndiv_algo_complete. unfold gt. apply (Nat.sub_le_mono_r (S (S n)) p (S n)) in H0. rewrite Nat.sub_succ_l in H0. rewrite Nat.sub_diag in H0. eapply Nat.le_trans. eapply H0. auto. auto. destruct (Ndiv_algo (p-S n) p). apply H1. auto. apply IHn. auto. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)