proposition: Lemma example m p : prime p -> p %| m `! + 1 -> m < p.
proof: Proof. move=> prime_p. apply: contraLR. rewrite -leqNgt. move=> leq_p_m. rewrite dvdn_addr. by rewrite gtnNdvd // prime_gt1. apply: dvdn_fact. by rewrite leq_p_m prime_gt0. Qed.
imports: mathcomp(all_ssreflect)