proposition: Lemma restrictE (T : finType) (e : rel T) (A : pred T) : A =i predT -> connect (restrict A e) =2 connect e.
proof: Proof. move => H x y. rewrite (eq_connect (e' := e)) //. move => {x y} x y /=. by rewrite !H. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)