Module docstring
{"# Further lemmas about integer division, now that omega is available.
","### dvd ","### *div zero ","### preliminaries for div equivalences ","### div equivalences ","### mod zero ","### mod definitions ","### mod equivalences ","### / ediv ","### emod ","### properties of / and % ","### / and ordering ","### tdiv ","There are no lemmas
* add_mul_tdiv_right : c ≠ 0 → (a + b * c).tdiv c = a.tdiv c + b
* add_mul_tdiv_left : b ≠ 0 → (a + b * c).tdiv b = a.tdiv b + c
* (similarly mul_add_tdiv_right, mul_add_tdiv_left)
* add_tdiv_of_dvd_right : c ∣ b → (a + b).tdiv c = a.tdiv c + b.tdiv c
* add_tdiv_of_dvd_left : c ∣ a → (a + b).tdiv c = a.tdiv c + b.tdiv c
because these statements are all incorrect, and require awkward conditional off-by-one corrections.
","### tmod ","properties of tdiv and tmod ","### tdiv and ordering ","### fdiv ","One could prove the following, but as the statements are quite awkward, so far it doesn't seem worthwhile.
```
theorem natAbs_fdiv {a b : Int} (h : b ≠ 0) :
natAbs (a.fdiv b) = a.natAbs / b.natAbs + if a.sign = b.sign ∨ b ∣ a then 0 else 1 := ...
theorem sign_fdiv (a b : Int) :
sign (a.fdiv b) = if a.sign = b.sign ∧ natAbs a < natAbs b then 0 else sign a * sign b := ...
``
","### fmod ","### properties offdivandfmod","###fdivand ordering ","### bmod ","Helper theorems fordvd` simproc "}