equal
deleted
inserted
replaced
141 on the natural numbers: |
141 on the natural numbers: |
142 \begin{isabelle} |
142 \begin{isabelle} |
143 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n) |
143 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n) |
144 \rulename{mod_if}\isanewline |
144 \rulename{mod_if}\isanewline |
145 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m% |
145 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m% |
146 \rulenamedx{mod_div_equality} |
146 \rulenamedx{div_mult_mod_eq} |
147 \end{isabelle} |
147 \end{isabelle} |
148 |
148 |
149 Many less obvious facts about quotient and remainder are also provided. |
149 Many less obvious facts about quotient and remainder are also provided. |
150 Here is a selection: |
150 Here is a selection: |
151 \begin{isabelle} |
151 \begin{isabelle} |