proposition: Lemma iso_graph_maxU (U := (union (iso_graphs))): domain U = substrate r1 \/ range U = substrate r2.
proof: Proof. move:(proj1 wor1) (proj1 wor2) => or1 or2. case: (equal_or_not (domain U) (substrate r1)) => ha; first by left. case: (equal_or_not (range U) (substrate r2)) => hb; first by right. move:iso_graph_stableU; rewrite -/U => Ud. move/Zo_P: (Ud) =>[/setP_P sU [Ua Ub Uc Ue]]. set Xa := substrate r1 -s (domain U). set Xb := substrate r2 -s (range U). have Xas: sub Xa (substrate r1) by apply: sub_setC. have Xbs: sub Xb (substrate r2) by apply: sub_setC. have neXa: (nonempty Xa) by apply: setC_ne; split => //; case: Ub. have neXb: (nonempty Xb) by apply: setC_ne; split => //; case: Uc. move:(worder_prop wor1 Xas neXa) =>[a /setC_P[asr anX] al]. move:(worder_prop wor2 Xbs neXb) =>[b /setC_P[bsr bnX] bl]. set g := U +s1 (J a b). have jabg: inc (J a b) g by apply: setU1_1. suff: (inc g iso_graphs). move => bad; move: (setU_s1 bad); rewrite -/U => /domain_S sg. case: anX; exact: (sg _ (domain_i jabg)). move: Ub Uc =>[qa qb] [qc qd]. have rre: sub g (substrate r1 \times substrate r2). by move => t /setU1_P; case; [ apply: sU | move => ->; apply:setXp_i]. have ra: sgraph g. move => t/setU1_P; case; [ fprops | move ->; fprops]. have rb: segmentp r1 (domain g). rewrite /g domain_setU1; split; first by apply:setU1_sub. move => x y /setU1_P xs xy; case: xs => xdu. apply:setU1_r; apply:(qb _ _ xdu xy). case: (inc_or_not y (domain U)) => ydU; first by apply: setU1_r. have yXa: inc y Xa by apply/setC_P; split => //; order_tac. move: (al _ yXa) => lay; rewrite xdu in xy. have -> : y = a by order_tac. fprops. have rc: segmentp r2 (range g). rewrite /g range_setU1; split; first by apply:setU1_sub. move => x y /setU1_P xs xy; case: xs => xdu. apply:setU1_r; apply:(qd _ _ xdu xy). case: (inc_or_not y (range U)) => ydU; first by apply: setU1_r. have yXa: inc y Xb by apply/setC_P; split => //; order_tac. move: (bl _ yXa) => lay; rewrite xdu in xy. have -> : y = b by order_tac. fprops. apply:Zo_i; [ by apply/setP_P | split => // u v c d p1g p2g]. case/setU1_P: p1g => Ha; case/setU1_P:p2g => Hb. + by apply: Ue. + move: (pr12_def Hb) =>[-> ->]. move:(domain_i Ha) (range_i Ha) => ud vr. move:(qa _ ud) (qc _ vr) => usr vsr. split => le1. case:(total_order_pr2 (worder_total wor2) bsr vsr) => // ltbv. case:bnX; exact:(qd v b vr (proj1 ltbv)). case:(total_order_pr2 (worder_total wor1) asr usr) => // ltbv. case:anX; exact:(qb _ _ ud (proj1 ltbv)). + move: (pr12_def Ha) =>[-> ->]; split => le1. case: anX; exact: (qb _ _ (domain_i Hb) le1). case: bnX; exact: (qd _ _ (range_i Hb) le1). + move: (pr12_def Hb) =>[-> ->]; move: (pr12_def Ha) =>[-> ->]. by split => _; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)