proposition: Lemma fix_order_gt0 (x : T) : (fix_order x > 0) = (x \in fixset).
proof: Proof. rewrite /fix_order; case: eqP => [x_in|/negP/negPf->//]. by rewrite x_in; case: ex_minnP => -[|m]; rewrite ?inE//= => _; apply. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)