proposition: Lemma primeNsig (n : nat) : ~~ prime n -> (2 <= n)%N -> { d : nat | (1 < d < n)%N & (d %| n)%N }.
proof: Proof. move=> primeN_n le2n; case/pdivP: {+}le2n => d /primeP[lt1d prime_d] dvd_dn. exists d => //; rewrite lt1d /= ltn_neqAle dvdn_leq 1?andbT //; last first. by apply: (leq_trans _ le2n). by apply: contra primeN_n => /eqP <-; apply/primeP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)