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