proposition: Lemma le_enum_val A : {mono @enum_val A : i j / i <= j}.
proof: Proof. apply: le_mono => i j le_ij. rewrite /enum_val (set_nth_default (enum_default j)) -?cardE//. apply: (sorted_ltn_nth lt_trans); rewrite -?topredE/= -?cardE//. by rewrite lt_sorted_uniq_le enum_uniq/= sort_sorted. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)