proposition: Lemma pimset_card (aT rT : finType) (f : aT -> option rT) (A : {set aT}) : #|[set x : rT | [exists x0 in A, f x0 == Some x]]| <= #|A|.
proof: Proof. apply: (@leq_trans #|[set f x | x in A]|); last exact: leq_imset_card. rewrite -[X in X <= _](card_imset _ (@Some_inj _)). apply: subset_leq_card. apply/subsetP => ? /imsetP [?] /pimsetP [x0]. move => H /eqP <- ->. by rewrite imset_f. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)