proposition: Lemma lem_insert_perm : forall l x, Permutation (insert l x) (x :: l).
proof: Proof. induction l as [|y ? ?]. - eauto using Permutation. - intro x. simpl. destruct (Nat.leb_spec x y) as [H|H]; eauto using Permutation. Qed.
imports: Hammer(Tactics) Arith Lia Sorting.Permutation