proposition: Theorem Nleast_div_least : forall p q, p > 1 -> q > 1 -> q < p -> (q | p) -> Nleast_div p <= q.
proof: Proof. intros. apply Nleast_div_ge_least. auto. auto with arith. auto. auto with arith. apply Nle_plus in H. destruct H. rewrite H. rewrite Nat.add_comm at 2. rewrite Nat.add_sub. rewrite Nat.add_sub. auto. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)