proposition: Lemma in_iter_ffixE (x : T) k : (x \in iterF k) = (0 < ffix_order x <= k).
proof: Proof. rewrite /ffix_order fset_iterFE; case: eqP => [xU|/negP xNU]; by [rewrite in_fset_valF|rewrite in_fset_valT /= in_iter_fixE]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)