proposition: Lemma subset_image (f : T -> U) A (Y : set U) : f @` A `<=` Y <-> forall a, A a -> Y (f a).
proof: Proof. split=> H. - by move=> a Xa; apply/H/imageP. - by move=> b [] a Xa <-; apply H. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp classical_sets)