proposition: Lemma pdiv_min_dvd m d : 1 < d -> d %| m -> pdiv m <= d.
proof: Proof. case: (posnP m) => [->|mpos] lt1d dv_d_m; first exact: ltnW. rewrite /pdiv; apply: leq_trans (pdiv_leq (ltnW lt1d)). have: pdiv d \in primes m. by rewrite mem_primes mpos pdiv_prime // (dvdn_trans (pdiv_dvd d)). case: (primes m) (sorted_primes m) => //= p pm ord_pm; rewrite inE. by case/predU1P => [-> | /(allP (order_path_min ltn_trans ord_pm)) /ltnW]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)