proposition: Lemma connect_restrict_mono (T : finType) (e : rel T) (A B : pred T) : A \subset B -> subrel (connect (restrict A e)) (connect (restrict B e)).
proof: Proof. move/subsetP => AB. apply: connect_mono => u v /=. rewrite -!andbA => /and3P [? ? ->]. by rewrite !AB. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)