proposition: Lemma max_pdiv_max n p : p \in \pi(n) -> p <= max_pdiv n.
proof: Proof. rewrite /max_pdiv !inE => n_p. case/splitPr: n_p (sorted_primes n) => p1 p2; rewrite last_cat -cat_rcons /=. rewrite headI /= cat_path -(last_cons 0) -headI last_rcons; case/andP=> _. move/(order_path_min ltn_trans); case/lastP: p2 => //= p2 q. by rewrite all_rcons last_rcons ltn_neqAle -andbA => /and3P[]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)