proposition: Lemma ord_fresh n (s : seq 'I_n) : size s < n -> exists k : 'I_n, k \notin s.
proof: Proof. move => H. suff: 0 < #|[predC s]|. { case/card_gt0P => z. rewrite !inE => ?; by exists z. } rewrite -(ltn_add2l #|s|) cardC addn0 card_ord. apply: leq_ltn_trans H. exact: card_size. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)