Library Coq.Arith.MinMax
Maximum and Minimum of two natural numbers
Fixpoint max n m :
nat :=
match n,
m with
|
O,
_ =>
m
|
S n',
O =>
n
|
S n',
S m' =>
S (
max n' m')
end.
Fixpoint min n m :
nat :=
match n,
m with
|
O,
_ => 0
|
S n',
O => 0
|
S n',
S m' =>
S (
min n' m')
end.
These functions implement indeed a maximum and a minimum
We obtain hence all the generic properties of max and min,
see file GenericMinMax or use SearchAbout.
Properties specific to the nat domain
Simplifications
Compatibilities (consequences of monotonicity)