proposition: Lemma plift_path (c1 : configuration q n) cs : path (move r2) (plift c1) [seq plift i | i <- cs] = path (move r1) c1 cs.
proof: Proof. elim: cs c1 => //= c2 cs IH c1. by rewrite plift_move IH. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)