proposition: Lemma fgraphsP X Y f: inc f (fgraphs X Y) <-> [/\ fgraph f, sub (domain f) X & sub (range f ) Y].
proof: Proof. split. move=> /Zo_P [/setP_P ha hb]. by split => // x /funI_P [ y /ha/setX_P[_ p q] -->]. move =>[ha hb hc]; apply: Zo_i => //; apply/setP_P => t tg. apply /setX_P; split. - exact: (proj1 ha _ tg). - by apply: hb; apply: funI_i. - by apply: hc; apply: funI_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)