proposition: Lemma root_partitionE : root_partition = equivalence_partition (connect e) A.
proof: Proof. apply/setP => B; apply/imsetP/imsetP => -[x Hx ->]. move: Hx => /set_inP[x_A root_x]; exists x => //; apply/setP => y. by rewrite !inE andb_idl // => xy; rewrite -(closed_connect closed_A xy). exists (root e x); first by rewrite !inE closed_root Hx roots_root. apply/setP => y; rewrite !inE andb_idl => [|xy]. apply: same_connect => //; exact: connect_root. by rewrite -(closed_connect closed_A xy). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)