diff options
| author | Antonio Nikishaev | 2019-09-28 23:35:26 +0300 |
|---|---|---|
| committer | Assia Mahboubi | 2019-09-28 22:35:26 +0200 |
| commit | d3dc7c337f2f031cec57d1f8804d59662e36ecfb (patch) | |
| tree | ca4dc16f0b9a65450a5c4b3826c5a849a1838cac /mathcomp | |
| parent | 50856f013e47c6469bb9c05300c48d94db121195 (diff) | |
maxn comment fix (#385)
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 5b667f0..3b7524e 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -62,7 +62,7 @@ Require Export Ring. (* *) (* maximum and minimum *) (* maxn m n, minn m n *) -(* Note that maxn m n = m + (m - n), due to the truncating subtraction. *) +(* Note that maxn m n = m + (n - m), due to the truncating subtraction. *) (* Absolute difference (linear distance) between nats is defined in the int *) (* library (in the int.IntDist sublibrary), with the syntax `|m - n|. The *) (* '-' in this notation is the signed integer difference. *) |