proposition: Lemma enum_ord_inord m : (enum 'I_m.+1) = [seq inord i | i <- iota 0 m.+1].
proof: Proof. rewrite -val_ord_enum -map_comp /=. rewrite enumT unlock /=. elim: (ord_enum _) => //= a l <-. by rewrite inord_val. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)