proposition: Lemma fconnect_sym_in : {in S &, forall x y, fconnect f x y = fconnect f y x}.
proof: Proof. suff Sf : {in S &, forall x y, fconnect f x y -> fconnect f y x}. by move=> *; apply/idP/idP=> /Sf->. move=> x _ xS _ /connectP [p f_p ->]; elim: p => //= y p IHp in x xS f_p *. case/andP: f_p => /eqP <- /(IHp _ (f_in xS)) /connect_trans -> //. by apply: (connect_trans (fconnect_finv _)); rewrite finv_f_in. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)