proposition: Lemma set_leP a b: a <=s b <-> equipotent_to_subset a b.
proof: Proof. rewrite/equipotent_to_subset; split. move=> [f [injf srf tgf]]. exists (Imf f). rewrite -tgf; apply: Imf_Starget; fct_tac. by rewrite /Imf - srf; apply:(Eq_restriction1 _ injf). move=> [z zy [f [[injf srj] sf tf]]]. exists ((canonical_injection z b) \co f). hnf; rewrite /canonical_injection; aw; split => //. by apply: inj_compose1=>//; [apply: ci_fi=>// | aw]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)