blob: a9882c88249636f0fdf0df9d8b646fd234a2e809 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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.
|
