proposition: Lemma predD_closed (e : rel T) (a b : {pred T}) : connect_sym e -> closed e a -> closed e b -> closed e [predD a & b].
proof: Proof. move=> sym_e cl_a cl_b; apply: intro_closed => // x y xy. by rewrite !inE (cl_a _ _ xy) (cl_b _ _ xy). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)