proposition: Lemma root_partitionP : partition root_partition A.
proof: Proof. rewrite root_partitionE equivalence_partitionP //. by apply:in3W; apply: connect_equivalence. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)