proposition: Lemma nth_ord (k n : nat) (A : {set 'I_k}) : n < #|A| -> { i : 'I_k | i \in A & #|[set j in A | j < i]| = n}.
proof: Proof. elim: n A => [|n IHn] A ltA; have [/= i0 i0A] := card_gtnE ltA. - pose i := [arg min_(i < i0 | i \in A) i]. exists i; rewrite /i; case: arg_minnP => // j jA min_j. apply/eq_card0 => o. by rewrite !inE; apply: contraTF isT => /andP[oA]; rewrite ltnNge min_j. - pose i := [arg min_(i < i0 | i \in A) i]. have [iA min_i] : i \in A /\ forall j, j \in A -> i <= j by rewrite /i; case: arg_minnP. rewrite (cardsD1 i) iA add1n ltnS in ltA. have [j /setD1P [jDi jA] <-] := IHn _ ltA. exists j; rewrite // [in LHS](cardsD1 i) inE iA ltn_neqAle eq_sym jDi min_i //=. by rewrite add1n; congr (_.+1); apply/eq_card => o; rewrite !inE -andbA eq_sym. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)