```
by
have hadd := Nat.div_add_mod (a + b) N
have hlt := @Nat.mod_lt (a + b) N (by linarith)
set r := (a + b) % N
set d := (a + b) / N
have : d ≤ 1 := by
nlinarith
interval_cases d <;> linarith
```
by
have hadd := Nat.div_add_mod (a + b) N
have hlt := @Nat.mod_lt (a + b) N (by linarith)
set r := (a + b) % N
set d := (a + b) / N
have : d ≤ 1 := by
nlinarith
interval_cases d <;> linarith
```
December 28, 2024 at 5:25 PM
```
by
have hadd := Nat.div_add_mod (a + b) N
have hlt := @Nat.mod_lt (a + b) N (by linarith)
set r := (a + b) % N
set d := (a + b) / N
have : d ≤ 1 := by
nlinarith
interval_cases d <;> linarith
```
by
have hadd := Nat.div_add_mod (a + b) N
have hlt := @Nat.mod_lt (a + b) N (by linarith)
set r := (a + b) % N
set d := (a + b) / N
have : d ≤ 1 := by
nlinarith
interval_cases d <;> linarith
```
My first instinct whenever I see a modulus in a problem like this is to use `Nat.div_add_mod` and `Nat.mod_lt`. After that I just bashed it with `linarith`.
December 28, 2024 at 5:25 PM
My first instinct whenever I see a modulus in a problem like this is to use `Nat.div_add_mod` and `Nat.mod_lt`. After that I just bashed it with `linarith`.