proposition: Lemma lem_isort_perm : forall l, Permutation (isort l) l.
proof: Proof. induction l; sauto use: lem_insert_perm. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation