proposition: Lemma restriction1_fb f x: injection f -> sub x (source f) -> bijection (restriction1 f x).
proof: Proof. move=> [ff fi] sxf; split; last by apply: restriction1_fs. have [pa pb pc] :=(restriction1_prop ff sxf). split => //; rewrite pb => a b ax bx. by rewrite ! restriction1_V=>//; apply: fi; apply: sxf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)