proposition: Lemma enum_ord_sorted_ltn N : sorted (fun i j : 'I_N => i < j) (enum 'I_N).
proof: Proof. rewrite /sorted; case Henum : (enum 'I_N) => [//= | a l]. rewrite -(map_path (h := val) (e := ltn) (b := pred0)) //. - rewrite (_ : l = behead (enum 'I_N)); last by rewrite Henum. rewrite (_ : val a = head 0 (map val (enum 'I_N))); last by rewrite Henum. rewrite -behead_map val_enum_ord. case: N {a l Henum} => [//= | N] /=. exact: (iota_ltn_sorted 0 N.+1). - by rewrite (eq_has (a2 := pred0)); first by rewrite has_pred0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(path) tools