proposition: Lemma notin_iter_ffix (x : T) k : k < ffix_order x -> x \notin iterF k.
proof: Proof. by move=> k_le; rewrite in_iter_ffixE negb_and orbC -ltnNge k_le. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)