proposition: Lemma iso_graph_stableU: inc (union (iso_graphs)) (iso_graphs).
proof: Proof. set U := union (iso_graphs). have ha x: inc x U -> inc x ((substrate r1) \times (substrate r2)). by move => /setU_P [y ya /Zo_S/setP_P]; apply. have hb x: inc x U -> pairp x by move => /ha/setX_P; case. apply: Zo_i; first by apply /setP_P. have q1: sgraph U. by move => t/setU_P [y ya /Zo_hi [gy _ _ _]]; apply: gy. have q4: segmentp r1 (domain U). rewrite domain_setU; apply: setU_segment => t/funI_P[ x xi ->]. by case/Zo_hi: xi. have q5: segmentp r2 (range U). rewrite range_setU; apply: setU_segment => t/funI_P[ x xi ->]. by case/Zo_hi: xi. split => //. move => a b c d /setU_P [x iax gx] /setU_P [y iby gy]. exact: (iso_graph_mon4 gx gy iax iby). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)