proposition: Lemma minset_fix : minset [pred X | F X == X] fixset.
proof: Proof. apply/minsetP; rewrite inE fixsetK eqxx; split=> // X /eqP FXeqX Xsubfix. apply/eqP; rewrite eqEsubset Xsubfix/=. suff: fixset \subset iter n F X by rewrite iter_fix. by rewrite /fixset; elim: n => //= [|m IHm]; rewrite ?sub0set ?F_mono. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)