proposition: Lemma perfect_eqE n k (p1 p2 : peg k) : (`c[p1, n.+1] == `c[p2]) = (p1 == p2).
proof: Proof. apply/eqP/eqP => [|<-] // cp1Ecp2. rewrite -(_ : `c[p1, n.+1] sdisk = p1); last by rewrite ffunE. by rewrite cp1Ecp2 ffunE. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)