proposition: Lemma ex5 n m : n`! + 2 <= m <= n`! + n -> ~~ prime m.
proof: Proof. move=> m_in; move: (m_in); rewrite -[m](@subnKC n`!); last first. by rewrite (@leq_trans (n`! + 2)) ?leq_addr//; by case/andP: m_in. set k := (_ - _); rewrite !leq_add2l => /andP[k_gt1 k_le_n]. apply/primePn; right; exists k. by rewrite k_gt1/= -subn_gt0 addnK fact_gt0. by rewrite dvdn_add// dvdn_fact// k_le_n (leq_trans _ k_gt1). Qed.
imports: mathcomp(all_ssreflect)