proposition: Lemma isubgraph_comp (F G H : diGraph) (i : F ⇀ G) (j : G ⇀ H) : F ⇀ H.
proof: Proof. apply: ISubgraph (j \o i) _ _. exact: inj_comp (isubgraph_inj j) (isubgraph_inj i). abstract by move=> x y /=; rewrite !isubgraph_mono. Defined.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)