proposition: Lemma sub_restrict_connect (T : finType) (e : rel T) (a : pred T) : subrel (connect (restrict a e)) (connect e).
proof: Proof. apply: connect_mono. exact: sub_restrict. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)