proposition: Lemma plift_move (c1 c2 : configuration q n) : move r2 (plift c1) (plift c2) = move r1 c1 c2.
proof: Proof. apply/moveP/moveP => [] [x [H1x H2x H3x H4x]]; exists x; split => //. - by rewrite !ffunE in H1x; rewrite -r2Rr1. - by move=> d2 xDd2; have := H2x _ xDd2; rewrite !ffunE => /lift_inj. - by rewrite plift_on_top in H3x. - by rewrite plift_on_top in H4x. - by rewrite !ffunE r2Rr1. - by move=> d2 /H2x; rewrite !ffunE => ->. - by rewrite plift_on_top. by rewrite plift_on_top. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)