proposition: Lemma mono_unique d (T T' : finPOrderType d) (f g : T -> T') : total (<=%O : rel T) -> (#|T'| <= #|T|)%N -> {mono f : x y / x <= y} -> {mono g : x y / x <= y} -> f =1 g.
proof: Proof. move=> le_total leT'T lef leg x0; move: {+}x0. suff: finfun f = finfun g by move=> /ffunP + x => /(_ x); rewrite !ffunE. apply: (can_inj fgraphK); apply/val_inj => /=; rewrite !codomE. under eq_map do rewrite ffunE; under [RHS]eq_map do rewrite ffunE. have [finj ginj] := (inc_inj lef, inc_inj leg). have [f' fK f'K] := inj_card_bij finj leT'T. have [g' gK g'K] := inj_card_bij ginj leT'T. apply/eqP; have : [seq f i | i <- Order.enum T] = [seq g i | i <- Order.enum T]. apply: (@sorted_eq _ <=%O le_trans le_anti); rewrite ?mono_sorted_enum//. apply: uniq_perm; rewrite ?map_inj_uniq ?sort_uniq ?fintype.enum_uniq//. move=> x; apply/mapP/mapP => -[y _ ->]. by exists (g' (f y)); rewrite ?Order.mem_enum. by exists (f' (g y)); rewrite ?Order.mem_enum. move=> /eqP; rewrite !eq_map_all all_map [in X in _ -> X]all_map. by have /permPl/perm_all-> := perm_sort <=%O (fintype.enum T). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)