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