proposition: Theorem sort_permutation : forall l:list A, permutation (sort l) l.
proof: Proof. unfold sort in |- *; intros l; rewrite <- mk_singletons_length. pattern l at 3 in |- *; rewrite <- app_all_mk_singletons_eq. apply sort_aux2_permutation; auto. Qed.
imports: List Lia