proposition: Lemma move_ldisk n (c1 c2 : configuration n.+1) : move c1 c2 -> c1 ldisk != c2 ldisk -> ↓[c1] = ↓[c2].
proof: Proof. move=> c1Mc2 c10Dc20. apply/ffunP=> i; rewrite !ffunE /=. apply: move_disk1 c1Mc2 c10Dc20 _. apply/eqP/val_eqP => /=. by rewrite eqn_leq negb_and -ltnNge ltn_ord. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)