max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add Nat.div_add_mod

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-01 08:20:00 -07:00
parent 92382ea47b
commit d1022e5587
1 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Init/Data/Nat/Div.lean
View file

@ -9,7 +9,7 @@ import Init.WFTactics
import Init.Data.Nat.Basic
namespace Nat
private def div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
theorem div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
fun ⟨ypos, ylex⟩ => sub_lt (Nat.lt_of_lt_of_le ypos ylex) ypos
@[extern "lean_nat_div"]
@ -123,4 +123,15 @@ theorem mod_one (x : Nat) : x % 1 = 0 := by
| succ y => intro h; apply absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero y)
exact this _ h
theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m := by
rw [div_eq, mod_eq]
have h : Decidable (0 < n ∧ n ≤ m) := inferInstance
cases h with
| isFalse h => simp [h]
| isTrue h =>
simp [h]
have ih := div_add_mod (m - n) n
rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2]
decreasing_by apply div_rec_lemma; assumption
end Nat