Library Coq.Arith.Min
THIS FILE IS DEPRECATED. Use
NPeano.Nat
instead.
Require
Import
NPeano
.
Local
Open
Scope
nat_scope
.
Implicit
Types
m
n
p
:
nat
.
Notation
min
:=
Peano.min
(
only
parsing
).
Definition
min_0_l
:=
Nat.min_0_l
.
Definition
min_0_r
:=
Nat.min_0_r
.
Definition
succ_min_distr
:=
Nat.succ_min_distr
.
Definition
plus_min_distr_l
:=
Nat.add_min_distr_l
.
Definition
plus_min_distr_r
:=
Nat.add_min_distr_r
.
Definition
min_case_strong
:=
Nat.min_case_strong
.
Definition
min_spec
:=
Nat.min_spec
.
Definition
min_dec
:=
Nat.min_dec
.
Definition
min_case
:=
Nat.min_case
.
Definition
min_idempotent
:=
Nat.min_id
.
Definition
min_assoc
:=
Nat.min_assoc
.
Definition
min_comm
:=
Nat.min_comm
.
Definition
min_l
:=
Nat.min_l
.
Definition
min_r
:=
Nat.min_r
.
Definition
le_min_l
:=
Nat.le_min_l
.
Definition
le_min_r
:=
Nat.le_min_r
.
Definition
min_glb_l
:=
Nat.min_glb_l
.
Definition
min_glb_r
:=
Nat.min_glb_r
.
Definition
min_glb
:=
Nat.min_glb
.