proposition: Lemma apegD p1 p2 m n : a[p1, p2] (m + n) = a[ a[p1, p2] n, a[p2, p1] n] m.
proof: Proof. by rewrite /apeg oddD; do 2 case: odd. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)