proposition: Lemma iter_sub_fix k : iterF k \subset fixset.
proof: Proof. have [/set_iterF_mono//|/ltnW/subnK<-] := leqP k n; by rewrite iterD fixsetKn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)