proposition: Lemma path_tuc (c : configuration _ _) cs : path (move rel) c cs -> path (move rel) (ctuc c) (rm_rep (ctuc c) [seq (ctuc i) | i <- cs]).
proof: Proof. elim: cs c => //= c1 cs IH c => /andP[cMc1 c1Pcs]. case: eqP => [->|/eqP cDc1 /=]; first by apply: IH; rewrite ?c2V. by rewrite move_tuc => //=; first by apply: IH; rewrite ?c2V. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)