proposition: Lemma iso_graph_prop (f := iso_seg_fun): [/\ segmentp r1 (source f), segmentp r2 (target f), source f= substrate r1 \/ target f = substrate r2 & order_isomorphism f (induced_order r1 (source f)) (induced_order r2 (target f))].
proof: Proof. move: iso_graph_stableU iso_graph_maxU. rewrite /f/iso_seg_fun; aw; set U := union _ => gU alt. move: (gU) => /Zo_P[/setP_P s1][qa qb qc qd]; split => //. move: (iorder_osr (proj1 wor1) (proj1 qb)) =>[ora sra]. move: (iorder_osr (proj1 wor2) (proj1 qc)) =>[orb srb]. have ff: function (triple (domain U) (range U) U). apply: function_pr => //; split => // u v uU vU sp1. move: (qa _ uU) (qa _ vU) => sa sb. apply: pair_exten => //. by move: uU vU; rewrite -{1} sa - {1} sb - sp1; apply: iso_graph_inj2. have fv z: inc z U -> Q z = Vg U (P z). move => zU. apply: select_uniq. + move => a b /funI_P [ap apu ->] eqa /funI_P [bp bpu ->] eqb. exact:(iso_graph_inj2 gU eqa eqb). + apply/funI_P; ex_tac. + by rewrite (qa _ zU). have bf: bijection (triple (domain U) (range U) U). split; saw. move => u v uU vU //; rewrite /Vf; aw. move/funI_P: uU =>[pa pau pav]. move/funI_P: vU =>[pb pbu pbv]. rewrite pav pbv - (fv _ pau) - (fv _ pbu) => eq1. move:(qa _ pau)(qa _ pbu) => p1 p2. move: pau pbu; rewrite -{1} p1 -{1} p2 - pav - pbv - eq1 => ia ib. exact (iso_graph_inj1 gU ia ib). move => y /funI_P [z zU ->]. exists (P z); first by apply/funI_P; ex_tac. by rewrite/Vf; aw; apply: fv. split => //; first by rewrite sra srb; saw. move => u v; aw => ud vd; rewrite /Vf; aw. move/funI_P:(ud) =>[up upU upv]. move/funI_P:(vd) =>[vp vpU vpv]. rewrite{2} upv - (fv _ upU) {2} vpv - (fv _ vpU). have ur: inc (Q up) (range U) by apply/funI_P; exists up. have vr: inc (Q vp) (range U) by apply/funI_P; exists vp. move:(qa _ upU)(qa _ vpU) => p1 p2. move: (upU)(vpU); rewrite -{1} p1 - {1} p2 => sa sb. move:(qd (P up) (Q up) (P vp) (Q vp) sa sb); rewrite - upv - vpv => mn. split. by move/iorder_gle1 => /mn le; apply/iorder_gleP. by move/iorder_gle1 => /mn le; apply/iorder_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)