proposition: Lemma in_iter_fix_orderE (x : T) : (x \in iterF (fix_order x)) = (x \in fixset).
proof: Proof. rewrite /fix_order; case: eqP; last by move=>/negP/negPf->; rewrite inE. by move=> x_in; case: ex_minnP => m ->; rewrite x_in. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)