proposition: Lemma half_le4 n: n <= n./2 -> n <= 1.
proof: Proof. by apply: contraLR; rewrite -!ltnNge; apply: half_le3w. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)