proposition: Lemma apeg32E a p1 p2 : a[p1, p2] (3 * a).-2 = a[p1, p2] a.
proof: Proof. case: a => // a. rewrite /apeg -subn2 oddB; last by rewrite mulnS. by rewrite oddM /=; case: odd. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)