proposition: Lemma fconnect_iter n x : fconnect f x (iter n f x).
proof: Proof. apply/connectP. by exists (traject f (f x) n); [apply: fpath_traject | rewrite last_traject]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)