proposition: Lemma mono_sorted_enum d d' (T : finPOrderType d) (T' : porderType d') (f : T -> T') : total (<=%O : rel T) -> {mono f : x y / (x <= y)%O} -> sorted <=%O [seq f x | x <- Order.enum T].
proof: Proof. move=> /sort_sorted ss_sorted lef; wlog [x0 x'0] : / (T * T')%type. by case: (Order.enum T) => // x ? => /(_ (x, f x)). rewrite (sorted_pairwise le_trans). apply/(pairwiseP x'0) => i j; rewrite !inE !size_map -!Order.cardT. move=> ilt jlt ij; rewrite !(nth_map x0) -?Order.cardT// lef. by rewrite (sorted_leq_nth le_trans le_refl) ?inE -?Order.cardT// 1?ltnW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)