proposition: Fact quasi_bij_prop f I J g (F := (Lf f I J)) (G := Lg J g) : quasi_bij f I J -> [/\ target F = domain G, bijection F & G \cf (graph F) = Lg I (fun z => Vg G (f z))].
proof: Proof. move=> [p1 p2 p3]. rewrite /F /G; saw; first by apply: lf_bijective. rewrite /Lf corresp_g /composef Lgd; apply: Lg_exten => i ij. by rewrite (LgV ij). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)