proposition: Lemma gdist_liftln m n (c1 c2 : configuration q m) : connect (move r1) c1 c2 -> gdist (move r2) (cliftln n p (plift p c1)) (cliftln n p (plift p c2)) <= gdist (move r1) c1 c2.
proof: Proof. move=> /gpath_connect[p1 p1H]. rewrite (gpath_dist p1H) -(size_map (cliftln n p \o plift p)). apply: gdist_path_le; first by rewrite path_liftln (gpath_path p1H). by rewrite [LHS]last_map (gpath_last p1H). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)