proposition: Lemma isubgraph_complLR (F G : sgraph) (i : compl F ⇀ G) : F ⇀ compl G.
proof: Proof. have I := isubgraph_inj i; apply: (@ISubgraph F (compl G) i) => // x y. exact: isubgraph_compLR_mono. Defined.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)