Fixpoint fileSectionOrderingCountLast
  (xs : list FileSectionDescriptionT)
  (n  : nat)
: nat :=
  match xs with
  | nil       => 0
  | cons y ys =>
    match (fileSectionOrdering y) with
    | FSO_MustBeLast => fileSectionOrderingCountLast ys (S n)
    | _              => fileSectionOrderingCountLast ys n
    end
  end.
