proposition: Lemma idvalue_P f x: function f -> sub x (source f) ->forall y, inc y (inverse_direct_value f x) <-> (inc y (source f) /\ (exists2 z, inc z x & Vf f y = Vf f z)).
proof: Proof. move => ff sxf. split. move /dirim_P => [u]; aw; move /dirim_P => [z zx pa] /igraph_pP pb. split; [Wtac | by ex_tac; rewrite - (Vf_pr ff pa) - (Vf_pr ff pb) ]. move => [ysf [z zx pa]]. apply/dirim_P; exists (Vf f z). apply/dirim_P;ex_tac; Wtac. aw; apply/igraph_pP; rewrite -pa; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)