proposition: Lemma lem_perm_sym {A} : forall l1 l2 : list A, Permutation l1 l2 -> Permutation l2 l1.
proof: Proof. induction 1; sauto. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation