proposition: Theorem Nleast_div_gt_1 : forall p, p > 1 -> 1 < Nleast_div p.
proof: Proof. intros. apply Nleast_div_ge_gt_1. auto. unfold lt. assert(p>=2). auto with arith. apply Nle_plus in H0. destruct H0. rewrite H0. rewrite Nat.add_comm at 1. rewrite Nat.add_sub. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)