proposition: Lemma exercise4_1b g: sgraph g -> (functional_graph g <-> (forall x y, disjoint x y -> disjoint (inverse_image g x) (inverse_image g y))).
proof: Proof. rewrite /disjoint;move=> gg; split. move /(exercise4_1a gg) => h x y ie; rewrite /disjoint -h ie. by rewrite /inverse_image dirim_set0. move=> hyp x y y' gxy gxy'. have gig: sgraph (inverse_graph g) by fprops. case: (emptyset_dichot ((singleton y) \cap (singleton y'))). move=>aux; move:(hyp _ _ aux). set v:= _ \cap _ => ve. have: (inc x v) by rewrite /v; apply: setI2_i; apply /iim_graph_P; ex_tac. by rewrite ve => /in_set0. by move=> [z /setI2_P [/set1_P -> /set1_P ->]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)