proposition: Lemma Permutation_vs_cons_inv : forall l l1 a, Permutation l (a :: l1) -> exists l' l'', l = l' ++ a :: l''.
proof: Proof. intros l l1 a HP. rewrite <- (app_nil_l (a :: l1)) in HP. apply (Permutation_vs_elt_inv _ _ _ HP). Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat