proposition: Lemma induced_forest (G : sgraph) (F : {set G}) : is_forest F -> is_forest [set: induced F].
proof: Proof. move => forest_F. apply: unique_forestT => x y p q Ip Iq. have [p0 /subsetP p0_sub_F eq_p0] := (Path_from_induced p). have [q0 /subsetP q0_sub_F eq_q0] := (Path_from_induced q). have ?: irred p0 by rewrite irredE eq_p0 map_inj_uniq //; exact: val_inj. have ?: irred q0 by rewrite irredE eq_q0 map_inj_uniq //; exact: val_inj. have Epq : p0 = q0 by apply: forest_F. apply/eqP; rewrite -nodes_eqE; apply/eqP. apply: (inj_map val_inj). by rewrite -eq_p0 -eq_q0 Epq. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)