proposition: Lemma rootP x y : reflect (root x = root y) (connect x y).
proof: Proof. apply: (iffP idP) => e_xy. by rewrite /root -(eq_pick (same_connect e_xy)); case: pickP e_xy => // ->. by apply: (connect_trans (connect_root x)); rewrite e_xy sym_e connect_root. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)