proposition: Lemma is_forestP S : reflect (is_forest S) (is_forestb S).
proof: Proof. apply: (iffP idP) => [H x y p q [Ip Sp] [Iq Sq]|H]. move/forallP/(_ x)/forallP/(_ y) : H => H. suff: Sub p Ip == Sub q Iq :> IPath x y by rewrite -val_eqE => /eqP. apply/eqP. apply:(card_le1_eqP H); by rewrite inE. - apply/forallP => x. apply/forallP => y. apply/card_le1_eqP => [[p Ip]] [q Iq]. rewrite !inE /= => pS qS. apply: val_inj => /=. exact: H. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)