proposition: Lemma Permutation_app_tail : forall (l l' tl : list A), Permutation l l' -> Permutation (l++tl) (l'++tl).
proof: Proof. intros l l' tl Hperm; induction Hperm as [|x l l'|x y l|l l' l'']; simpl; auto. eapply Permutation_trans with (l':=l'++tl); trivial. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat