proposition: Lemma sorted_enum_val (m : nat) (s : {set 'I_m}) (i j : 'I_#|s|) : (enum_val i) < (enum_val j) = (i < j).
proof: Proof. case: m s i j => [s|m s i j]. rewrite (_ : s = set0). case=> m H j; apply: False_ind. by rewrite cards0 in H. by apply/setP=> [] []. have := ltn_ord i; have := ltn_ord j; rewrite {2 4}cardE. rewrite /enum_val /= /(enum _) -enumT enum_ord_inord => iL jL. have <-// := @nth_map ('I_m.+1) (enum_default i) nat 0 (@nat_of_ord m.+1). have <-// := @nth_map ('I_m.+1) (enum_default j) nat 0 (@nat_of_ord m.+1). have F k1 k2 : k1 + k2 <= m.+1 -> [seq (nat_of_ord i) | i <- [seq inord i0 | i0 <- iota k1 k2] & mem s i] = (filter (fun i0 => mem s (inord i0)) (iota k1 k2)). elim: k2 k1 => //= k2 IH k1 k1k2Lm. case: (_ \in _) => //=. rewrite inordK //. rewrite IH //. by rewrite addSnnS. by apply: leq_trans k1k2Lm; rewrite -addSnnS leq_addr. apply: IH. by rewrite addSnnS. rewrite F //. have : j < size ([seq i0 <- iota 0 m.+1 | mem s (inord i0)]). by move: iL; rewrite -F // size_map. have : i < size ([seq i0 <- iota 0 m.+1 | mem s (inord i0)]) by move: jL; rewrite -F // size_map. apply: sorted_filter => //. by apply: sorted_iota. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)