proposition: Lemma lem_perm_length {A} : forall l1 l2 : list A, Permutation l1 l2 -> List.length l1 = List.length l2.
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