proposition: Lemma fix_order_le_max (x : T) : fix_order x <= n.
proof: Proof. rewrite /fix_order; case: eqP => //= x_in. by case: ex_minnP => //= ??; apply. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)