proposition: Lemma Sprod_range A B: sgraph A -> sgraph B -> (range (Sprod A B)) = ((range A) \times (range B)).
proof: Proof. move => ga gb. apply: extensionality. move => x /funI_P [z /Sprod_P [a [b [c [d [ha hb hc]]]]] ->]. by rewrite hc pr2_pair; apply: setXp_i; apply /funI_P; ex_tac; aw. move => x /setX_P [pp /funI_P[ a hb hc] /funI_P [b he hf]]. apply/funI_P; exists (J (J (P a) (P b)) x); aw; trivial. rewrite - pp hc hf; apply/Sprod_P. exists (P a), (P b), (Q a), (Q b); split => //. - by rewrite (ga _ hb). - by rewrite (gb _ he). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)