proposition: Lemma eq_closed_r (e : rel T) (a b : {pred T}) : a =i b -> closed e a <-> closed e b.
proof: Proof. by rewrite /closed_mem => ab; split => -cl x y /cl; rewrite !ab. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)