proposition: Lemma move_connect_lpeg n (c : configuration _ n) p : `c[p] `-->*_r c.
proof: Proof. rewrite [connect _ _ _]connect_sym //. by apply: move_connect_rpeg. by exact: rsym. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)