proposition: Lemma ffix_order_gt0 (x : T) : (ffix_order x > 0) = (x \in fixfset).
proof: Proof. rewrite /ffix_order; case: eqP => [xU|/negP xNU]; last by rewrite in_fset_valF. by rewrite fix_order_gt0 in_fset_valT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)