proposition: Lemma restriction_to_image_fb f: injection f -> bijection (restriction_to_image f).
proof: Proof. by move => h; rewrite (restriction_to_imageE (proj1 h));apply: restriction1_fb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)