proposition: Theorem Nleast_div_ge_gt_1 : forall n p, p > 1 -> S n < p -> 1 < Nleast_div_ge n p.
proof: Proof. induction n. intros. compute. auto. intros. simpl. destruct (Ndiv_algo (p-S n) p). apply (Nat.sub_le_mono_r (S(S(S n))) p (S n)) in H0. rewrite Nat.sub_succ_l in H0. rewrite Nat.sub_succ_l in H0. rewrite Nat.sub_diag in H0. auto. auto. auto. apply IHn. auto. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)