proposition: Lemma connect_mono (T : finType) (e1 e2 : rel T) : subrel e1 e2 -> subrel (connect e1) (connect e2).
proof: Proof. move => A. apply: connect_sub. exact: sub_trans (sub_connect e2). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)