proposition: Lemma move_disk1 n (d1 d2 : disk n) (c1 c2 : configuration n) : move c1 c2 -> c1 d1 != c2 d1 -> d1 != d2 -> c1 d2 = c2 d2.
proof: Proof. case/moveP=> d3 [H1 H2 H3 H4] c1d1Dc2d1 d1Dd2. have [/eqP d3Ed1|d3Dd1] := boolP (d3 == d1); last first. by case/eqP: c1d1Dc2d1; apply: H2. by apply: H2; rewrite d3Ed1. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)