proposition: Lemma exercise3_5 G A B: ((A \times B) \cg G = (inverse_image G A) \times B /\ G \cg (A \times B) = A \times (direct_image G B)).
proof: Proof. split; set_extens x. - move /compg_P => [px [y yG /setXp_P [pa pb]]]. apply/setX_P;split => //; apply/iim_graph_P; ex_tac. - move /setX_P => [px /iim_graph_P [y uA JG] QB]. apply /compg_P; split => //; ex_tac; fprops. - move /compg_P => [px [y /setXp_P [pa pb pc]]]. apply /setX_P;split => //; apply/dirim_P; ex_tac. - move /setX_P => [px pxa /dirim_P [y ya yb]]. apply/compg_P; split => //; ex_tac; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)