proposition: Lemma induced_isubgraph (G : sgraph) (A : {set G}) : induced A ⇀ G.
proof: Proof. pose f (x : induced A) : G := val x. have : {mono f : x y / x -- y} by abstract by move => x y; rewrite induced_edge. apply: ISubgraph; exact: val_inj. Defined.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)