proposition: Lemma corr_propcc s t g: sub g (s \times t) <-> [/\ sgraph g, sub (domain g) s & sub (range g) t].
proof: Proof. split => [sg | [gg sd sr] x xg ]. have gg:= (sub_setX_graph sg). by split =>// z /funI_P [y yp ->];move/setX_P: (sg _ yp) => [_]. rewrite -(gg _ xg); apply: setXp_i; [ apply: sd | apply: sr]; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)