proposition: Lemma enum_ord_sorted N : sorted (fun i j : 'I_N => i <= j) (enum 'I_N).
proof: Proof. by have:= enum_ord_sorted_ltn N; apply: sub_sorted => i j /=/ltnW. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(path) tools