proposition: Lemma move_unliftr n (c1 c2 : configuration n.+1) : c1 ldisk = c2 ldisk -> move ↓[c1] ↓[c2] = move c1 c2.
proof: Proof. by move=> c1lEc2l; rewrite -(@move_liftr _ (c1 ldisk)) {2}c1lEc2l !cunliftrK. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)