proposition: Theorem Permutation_app : forall (l m l' m' : list A), Permutation l l' -> Permutation m m' -> Permutation (l++m) (l'++m').
proof: Proof. intros l m l' m' Hpermll' Hpermmm'; induction Hpermll' as [|x l l'|x y l|l l' l'']; repeat rewrite <- app_comm_cons; auto. - apply Permutation_trans with (l' := (x :: y :: l ++ m)); [idtac | repeat rewrite app_comm_cons; apply Permutation_app_head]; trivial. - apply Permutation_trans with (l' := (l' ++ m')); try assumption. apply Permutation_app_tail; assumption. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat