proposition: Lemma restriction_to_image_fs f: function f -> surjection (restriction_to_image f).
proof: Proof. by move => h; rewrite (restriction_to_imageE h);apply: restriction1_fs. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)