proposition: Lemma move_liftr_perfect q n (hrel : rel (peg q)) p1 p2 p3 : hrel p1 p2 -> p1 != p3 -> p2 != p3 -> move hrel ↑[`c[p3, n]]_p1 ↑[`c[p3]]_p2.
proof: Proof. move=> p1Rp2 p1Dp3 p2Dp3. apply: (@move_mergel_inv _ _ 1). - by apply/cdisjointP => i j; rewrite !ffunE. - by apply/cdisjointP => i j; rewrite !ffunE. apply/moveP; exists ldisk; split; try by apply: on_top1. by rewrite !ffunE. by case => [] []. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)