proposition: Lemma change_target_pr f E (g:= change_target_fun f E): function f -> sub (target f) E -> (function_prop g (source f) E /\ forall x, inc x (source f) -> Vf g x = Vf f x).
proof: Proof. move => ff stf; rewrite /g/change_target_fun; saw. have h := (sub_trans (f_range_graph ff) stf). have [_ pc pb] := ff. saw; exact: function_pr. by move=> x xsf; rewrite /Vf; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)