proposition: Lemma isubgraph_compl (F G : sgraph) (i : F ⇀ G) : compl F ⇀ compl G.
proof: Proof. apply: isubgraph_complLR. exact: isubgraph_comp (iso_isubgraph (diso_compl F)) i. Defined.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)