proposition: Lemma restriction_fi f x y a: sub a x -> bijection_prop f x y -> injection_prop (restriction f a) a y.
proof: Proof. move =>sax [[[ff ha] _] sf <-]. have sxsf: sub a (source f) by rewrite sf. move: (restriction_prop ff sxsf) =>[qa qb qc]. split => //; split => // u v; rewrite qb => uv vx. by rewrite restriction_V // restriction_V //; apply: ha; apply: sxsf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)