proposition: Lemma leq_e2n m n : (`2^ m <= `2^ n) = (m <= n).
proof: Proof. elim: n m => [/= [|m]//|n IH [|m]]. - by rewrite e2Sn; case: e2n (e2n_gt0 m) => //= n; rewrite addnS. - rewrite (leq_trans _ (_ : `2^ 1 <= `2^ n.+1)) //. by rewrite !e2Sn !addnn (leq_double 1) e2n_gt0. by rewrite !e2Sn !addnn leq_double IH. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)