proposition: Lemma move_cset (c1 c2 : configuration k n) : move rel c1 c2 -> (cset c1) != (cset c2) -> move rel (cset c1) (cset c2).
proof: Proof. move => /moveP [d [dH1 dH2 dH3 dH4]] c1Dc2. have [dIsd|dNIsd] := boolP (d \in sd); last first. case/eqP: c1Dc2. apply/ffunP => i; rewrite !ffunE. apply: dH2. apply: contra dNIsd => /eqP->. by apply: enum_valP. apply/moveP; exists (enum_rank_in dIsd d); split => /=. - by rewrite !ffunE !enum_rankK_in //. - move=> /= d2 dDd2. rewrite !ffunE. apply: dH2. rewrite -[d](enum_rankK_in dIsd) //. by apply /eqP => /enum_val_inj /eqP; rewrite (negPf dDd2). - by apply: on_top_cset. by apply: on_top_cset. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)