proposition: Lemma path_clshift m n (c : configuration (m + n)) cs : path move c cs -> path move (clshift c) (rm_rep (clshift c) [seq (clshift i) | i <- cs]).
proof: Proof. elim: cs c => //= c1 cs IH c => /andP[cMc1 c1Pcs]. case: eqP => [->|/eqP cDc1 /=]; first by apply: IH. by rewrite move_clshift //=; apply: IH. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)