proposition: Lemma card_gtnE (T : finType) n (p : {pred T}) : n < #|p| -> { x | x \in p }.
proof: Proof. by move=> n_p; apply/sigW/card_gt0P; apply: leq_trans n_p. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)