Library Coq.Arith.Max
Require Import Le.
Open Local Scope nat_scope.
Implicit Types m n :
nat.
maximum of two natural numbers
Fixpoint max n m {
struct n} :
nat :=
match n,
m with
|
O,
_ =>
m
|
S n',
O =>
n
|
S n',
S m' =>
S (
max n' m')
end.
max n m is equal to n or m