proposition: Lemma ltn_ne2n n : n < `2^ n.
proof: Proof. elim: n => // [] [|n] // IH. apply: leq_ltn_trans (_ : n.+1.*2 < _). by rewrite -addnn addnS addSn !ltnS leq_addr. by rewrite e2Sn addnn ltn_double. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)