proposition: Lemma fix_order_big x k : x \in fixset -> x \notin iterF k -> fix_order x > k.
proof: Proof. by move=> x_in; rewrite in_iter_fixE fix_order_gt0 x_in /= -ltnNge. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)