proposition: Lemma connect_liftln m n (c1 c2 : configuration q m) : connect (move r1) c1 c2 -> connect (move r2) (cliftln n p (plift p c1)) (cliftln n p (plift p c2)).
proof: Proof. move=> /connectP[x]; rewrite -(path_liftln n) => Hp Hl. apply/connectP; eexists; first exact: Hp. by rewrite Hl [RHS]last_map. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)