proposition: Lemma permutation_singleton : forall {A} seq x, @Permutation A seq [x] -> seq = [x].
proof: Proof. induction seq; simpl; intros. apply Permutation_nil in H; intuition. pose proof (Permutation_length H) as len; simpl in len. inversion len. destruct seq; simpl in *; try discriminate. apply Permutation_length_1 in H; congruence. Qed.
imports: Coq.Sorting.Permutation Fiat.Common Coq.Lists.List Fiat.Common.List.ListFacts Coq.Program.Program