proposition: Lemma fconnect_eqVf x y : fconnect f x y = (x == y) || fconnect f (f x) y.
proof: Proof. apply/idP/idP => [/iter_findex <-|/predU1P [<-|] //]; last first. exact/connect_trans/fconnect1. by case: findex => [|i]; rewrite ?eqxx// iterSr fconnect_iter orbT. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)