proposition: Lemma in_iter_ffix_orderE (x : T) : (x \in iterF (ffix_order x)) = (x \in fixfset).
proof: Proof. rewrite /ffix_order; case: eqP => [xU|/negP xNU]; last first. by rewrite !inE /fixfset in_fset_valF. by rewrite fset_iterFE !in_fset_valT /= in_iter_fix_orderE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)