Module RBindingsNat
Section
RBindingsNat
.
Require
Import
Arith
.
Require
Import
NPeano
.
Require
Import
RBindings
.
Global
Program
Instance
ODT_nat
: (@
ODT
nat
)
:=
mkODT
_
_
lt
Nat.lt_strorder
lt_dec
Compare_dec.nat_compare
_
.
Next Obligation.
simpl
.
apply
Compare_dec.nat_compare_spec
.
Qed.
End
RBindingsNat
.
Hint
Unfold
rec_sort
rec_concat_sort
.
Hint
Resolve
drec_sort_sorted
drec_concat_sort_sorted
.
Hint
Resolve
is_list_sorted_NoDup_strlt
.