proposition: Lemma dvdn_e2n m n : (`2^ m %| `2^ n) = (m <= n).
proof: Proof. elim: n m => [[|m]//=|n IH [/=|m]]. - rewrite dvdn1. by rewrite eqn_leq leqNgt -add1n !addnn leq_double e2n_gt0. - by rewrite dvd1n. by rewrite !e2Sn !addnn -!muln2 dvdn_pmul2r // IH. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)