Properties of subtraction between natural numbers.
This file is mostly OBSOLETE now, see module
PeanoNat.Nat instead.
minus is now an alias for
Nat.sub, which is defined in
Init/Nat.v as:
Fixpoint sub (n m:nat) : nat :=
match n, m with
| S k, S l => k - l
| _, _ => n
end
where "n - m" := (sub n m) : nat_scope.