proposition: Lemma eq_connected (V : finType) (e1 e2 : rel V) (A : {set V}) (e1_sym : symmetric e1) (e1_irrefl : irreflexive e1) (e2_sym : symmetric e2) (e2_irrefl : irreflexive e2): e1 =2 e2 -> @connected (SGraph e1_sym e1_irrefl) A <-> @connected (SGraph e2_sym e2_irrefl) A.
proof: Proof. move => E. split. - move => H x y xA yA. erewrite eq_connect. eapply H => //. move => u v. by rewrite /edge_rel /= E. - move => H x y xA yA. erewrite eq_connect. eapply H => //. move => u v. by rewrite /edge_rel /= E. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)