proposition: Theorem permutation_app : forall l1 l2:list A, permutation (l1 ++ l2) (l2 ++ l1).
proof: Proof. intros l1; elim l1; simpl in |- *. - intros l2; rewrite app_nil_r. apply permutation_reflexive. - intros a tl Hrec l2. apply permutation_transitive with (a :: l2 ++ tl). + apply permutation_same_head. apply Hrec. + apply permutation_symmetric; apply permutation_app_cons. Qed.
imports: List Lia