proposition: Lemma ffix_order_le_max (x : T) : ffix_order x <= #|` U|.
proof: Proof. by rewrite /ffix_order; case: eqP => //= x_in; rewrite cardfE fix_order_le_max. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)