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