1 files changed, 18 insertions, 0 deletions
diff --git a/src/TAPSort.v b/src/TAPSort.v
new file mode 100644
index 000000000..a9882c882
--- /dev/null
+++ b/src/TAPSort.v
@@ -0,0 +1,18 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Sorting.Mergesort.
+
+
+Module TAPOrder <: Orders.TotalLeBool.
+  Local Coercion is_true : bool >-> Sortclass.
+  Definition t := (Z * Z)%type.
+  Definition leb (x y : t) := Z.geb (snd x) (snd y).
+  Infix "<=?" := leb.
+  Theorem leb_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1.
+  Proof.
+    intros; cbv [is_true leb]; rewrite !Z.geb_le; omega.
+  Qed.
+End TAPOrder.
+
+Module TAPSort := Sort TAPOrder.
+
+Notation sort := TAPSort.sort.