proposition: Lemma connectedP S : reflect (connected S) (connectedb S).
proof: Proof. apply: (iffP idP) => H. - move => x y xS yS. by move/forall_inP/(_ _ xS)/forall_inP/(_ _ yS) : H. - do 2 apply/forall_inP => ? ?. exact: H. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)