proposition: Lemma size_ppeg n p1 p2 : size (ppeg p1 p2 : seq (configuration 3 n)) = (2^ n).-1.
proof: Proof. elim: n p1 p2 => //= n IH p1 p2. rewrite size_cat /= !size_map !IH expnS mul2n -addnn. by rewrite -(prednK (_ : 0 < 2 ^ n)) // expn_gt0. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)