proposition: Lemma in_iter_ffix (x : T) k : x \in fixfset -> ffix_order x <= k -> x \in iterF k.
proof: Proof. by move=> x_in xk; rewrite in_iter_ffixE ffix_order_gt0 x_in xk. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)