proposition: Lemma restrict_sym (T : Type) (A : pred T) (e : rel T) : symmetric e -> symmetric (restrict A e).
proof: Proof. move => sym_e x y /=. by rewrite sym_e [(x \in A) && _]andbC. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)