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