proposition: Lemma restr_range f x: function f -> sub x (source f) -> sub (range (restr (graph f) x)) (target f).
proof: Proof. move=> ff sxdf t /funI_P [z /funI_P [s zg ->] ->]; aw;rewrite -/(Vf _ _); Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)