proposition: Lemma sub_forest S S' : S' \subset S -> is_forest S -> is_forest S'.
proof: Proof. move => subS H x y p q [Ip Sp] [Iq Sq]. apply: H; try split; try solve [ done |exact: (subsetP subS) | exact: subset_trans subS]. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)