proposition: Lemma fixsetK : F fixset = fixset.
proof: Proof. suff /'exists_eqP[x /= e]: [exists k : 'I_n.+1, iterF k == iterF k.+1]. by rewrite /fixset -(subnK (leq_ord x)) iterD iter_fix. apply: contraT; rewrite negb_exists => /forallP /(_ (Ordinal _)) /= neq_iter. suff iter_big k : k <= n.+1 -> k <= #|iter k F set0|. by have := iter_big _ (leqnn _); rewrite ltnNge max_card. elim: k => [|k IHk] k_lt //=; apply: (leq_ltn_trans (IHk (ltnW k_lt))). by rewrite proper_card// properEneq// set_iterF_sub neq_iter. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)