proposition: Lemma size_rpeg_up n (c : _ _ n) p : size_rpeg c p <= (2^ n).-1.
proof: Proof. elim: n c p => //= n IH c p. case: eqP => _. apply: (leq_trans (IH _ _)). case: (_ ^ _) (expn_eq0 2 n) (expn_eq0 2 n.+1) (leq_pexp2l (isT: 0 < 2) (ltnW (leqnn n.+1))) => //= n1 _. by case: (_ ^ _). apply: leq_trans (_ : (2^n).-1 + (2^n) <= _). by rewrite leq_add2r IH. rewrite expnS mul2n -addnn. by case: (2 ^ n) (expn_eq0 2 n) => [|n1]; rewrite ?addn0. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)