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