proposition: Theorem permutation_symmetric : forall l1 l2:list A, permutation l1 l2 -> permutation l2 l1.
proof: Proof. intros l1 l2 H; elim H; try (intros; constructor; assumption). intros l3 l4 l5; intros; apply permutation_transitive with l4; assumption. Qed.
imports: List Lia