proposition: Lemma in_iter_fixE (x : T) k : (x \in iterF k) = (0 < fix_order x <= k).
proof: Proof. rewrite /fix_order; case: eqP => //= [x_in|/negP xNin]; last first. by apply: contraNF xNin; apply/subsetP/iter_sub_fix. case: ex_minnP => -[|m]; rewrite ?inE// => xm mP. by apply/idP/idP=> [/mP//|lt_mk]; apply: subsetP xm; apply: set_iterF_mono. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)