proposition: Lemma fix_order_small x k : x \in iterF k -> fix_order x <= k.
proof: Proof. by rewrite in_iter_fixE => /andP[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)