fact: Definition sink_measure (Lj : (list A) * nat) : nat := match Lj with (L, j) => length L - j end.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset