proposition: Lemma isubgraph_compLR_mono (F G : sgraph) (i : compl F ⇀ G) (x y : F) : i x -- i y :> compl G = x -- y.
proof: Proof. have I := isubgraph_inj i. rewrite [LHS]/edge_rel/= isubgraph_mono [in LHS]/edge_rel/= inj_eq //. rewrite negb_and !negbK andb_orr andbC andbN orFb andb_idl //. by move/sg_edgeNeq ->. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)