proposition: Lemma ffix_order_big x k : x \in fixfset -> x \notin iterF k -> ffix_order x > k.
proof: Proof. by move=> x_in; rewrite in_iter_ffixE ffix_order_gt0 x_in -ltnNge. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)