Skip to content

Instantly share code, notes, and snippets.

@nomeata

nomeata/Sort.v

Created June 23, 2014 17:43
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save nomeata/e8d7190a9ae52f524c69 to your computer and use it in GitHub Desktop.
Save nomeata/e8d7190a9ae52f524c69 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment