proposition: Lemma codom_apeg (A : finType) (f : {ffun A -> _}) p1 p2 n : (codom f \subset [:: a[p1, p2] n; a[p2, p1] n]) = (codom f \subset [:: p1; p2]).
proof: Proof. by rewrite /apeg; case: odd; rewrite // codom_subC. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)