Sort.v

Theorem insert_perm: forall k l, Permutation (k :: l) (insert k l).
Proof.
  intros. induction l.
  - reflexivity.
  - simpl. destruct (ble_nat k a).
    + reflexivity.
    + transitivity (a :: k :: l).
      * apply perm_swap.
      * constructor; assumption.
Qed.