proposition: Lemma fpathP x p : reflect (exists n, p = traject f (f x) n) (fpath f x p).
proof: Proof. apply: (iffP idP) => [/fpathE->|[n->]]; first by exists (size p). by elim: n => //= n IHn in x *; rewrite eqxx IHn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)