proposition: Lemma Permutation_cons_append : forall (l : list A) x, Permutation (x :: l) (l ++ x :: nil).
proof: Proof. induction l; intros; auto. simpl. rewrite <- IHl; auto. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat