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