proposition: Lemma pi_max_pdiv n : (max_pdiv n \in \pi(n)) = (n > 1).
proof: Proof. rewrite !inE -pi_pdiv /max_pdiv /pdiv !inE. by case: (primes n) => //= p ps; rewrite mem_head mem_last. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)