proposition: Lemma move_connect_rpeg n (c : configuration _ n) p : c `-->*_r `c[p].
proof: Proof. apply/connectP; exists (rpeg c p); first by apply: path_rpeg. by rewrite last_rpeg. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)