proposition: Lemma hanoi_rep n : hanoi n = rep (2 ^ n).-1 tick.
proof: Proof. elim: n => // n IH /=. rewrite IH -repS prednK ?expn_gt0 // -rep_addn. by rewrite -subn1 addnBA ?expn_gt0 // addnn -muln2 -expnSr subn1. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy