proposition: Lemma move_diskr n (d : disk n) (c1 c2 : configuration n) : move c1 c2 -> c1 d != c2 d -> r (c1 d) (c2 d).
proof: Proof. case/moveP=> d1 [H1 H2 H3 H4] /eqP c1dDc2d. by have [/eqP<-|/H2] := boolP (d1 == d). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)