diff options
| -rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 277223f4bc..98809fbf8f 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -101,13 +101,13 @@ Fixpoint divmod x y q u := Definition div x y := match y with - | 0 => 0 + | 0 => y | S y' => fst (divmod x y' 0 y') end. Definition modulo x y := match y with - | 0 => 0 + | 0 => y | S y' => y' - snd (divmod x y' 0 y') end. |