proposition: Lemma move_connect n (c1 c2 : configuration 3 n) : c1 `-->*_r c2.
proof: Proof. by apply: connect_trans (move_connect_rpeg c1 (inord 1)) (move_connect_lpeg c2 (inord 1)). Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)