proposition: Lemma inj_card_onto_pred (aT rT : finType) (f : aT -> rT) (P : pred rT) : injective f -> (forall x, f x \in P) -> #|aT| = #|P| -> {in P, forall y, y \in codom f}.
proof: Proof. move => f_inj fP E y yP. pose rT' := { y : rT | P y}. pose f' (x:aT) : rT' := Sub (f x) (fP x). have/inj_card_onto : injective f' by move => x1 x2 []; exact: f_inj. case/(_ _ (Sub y yP))/Wrap => [|/codomP[x]]; first by rewrite card_sig E. by move/(congr1 val) => /= ->; exact: codom_f. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)