proposition: Lemma iso_graph_mon2 g a b c: inc g iso_graphs -> inc (J a b) g -> glt r1 c a -> exists2 d, glt r2 d b & inc (J c d) g.
proof: Proof. move => gi qa [qb qc]. move: (gi) => /Zo_P[/setP_P h [pa pb pc pd]]. have br: inc a (domain g) by apply/funI_P; ex_tac; aw. move:(proj2 pb _ _ br qb) =>/funI_P [db dg dv]. have ph: inc (J c (Q db)) g by rewrite dv (pa _ dg). exists (Q db) => //; split; first by apply/ (pd _ _ _ _ ph qa). move => bad. rewrite bad in ph. case: qc; exact:(iso_graph_inj1 gi ph qa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)