proposition: Lemma Permutation_vs_elt_inv : forall l l1 l2 a, Permutation l (l1 ++ a :: l2) -> exists l' l'', l = l' ++ a :: l''.
proof: Proof. intros l l1 l2 a HP. symmetry in HP. apply (Permutation_in a), in_split in HP; trivial. apply in_elt. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat