proposition: Lemma half_le3w m: 1 < m -> m./2 < m.
proof: Proof. move/half_le3 => h; exact: (leq_ltn_trans (half_leq (leqnSn m)) h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)