michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/nat/div): add characterization of mod

Browse source
This commit is contained in:
Jeremy Avigad 2015-06-27 18:51:44 +10:00
parent 829c3fb22c
commit f8d8a2aed6
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/data/nat/div.lean
View file

@ -186,6 +186,9 @@ by_cases_zero_pos y
... = succ x - y + y : {!(IH _ H6)⁻¹} ... = succ x - y + y : {!(IH _ H6)⁻¹}
... = succ x : sub_add_cancel H2)⁻¹))) ... = succ x : sub_add_cancel H2)⁻¹)))
theorem mod_eq_sub_div_mul (x y : ℕ) : x mod y = x - x div y * y :=
eq_sub_of_add_eq (!add.comm ▸ !eq_div_mul_add_mod)⁻¹
theorem mod_add_mod (m n k : ℕ) : (m mod n + k) mod n = (m + k) mod n := theorem mod_add_mod (m n k : ℕ) : (m mod n + k) mod n = (m + k) mod n :=
by rewrite [eq_div_mul_add_mod m n at {2}, add.assoc, add.comm (m div n * n), add_mul_mod_self] by rewrite [eq_div_mul_add_mod m n at {2}, add.assoc, add.comm (m div n * n), add_mul_mod_self]