## Stream: new members

### Topic: lemmas related to core

#### Yakov Pechersky (Aug 13 2020 at 14:33):

Where would something like the lemma below go? The mod_eq_of_lt is in core.

@[simp] lemma one_mod_eq_one (n : ℕ) : 1 % (n + 2) = 1 := by { exact nat.mod_eq_of_lt (add_lt_add_right n.succ_pos 1) }


#### Alex J. Best (Aug 13 2020 at 14:38):

data.nat.basic seems reasonable. (zero_mod for int is in data.int.basic for example)

#### Chris Wong (Aug 14 2020 at 08:45):

I think you can drop the exact and use term mode directly

#### Chris Wong (Aug 14 2020 at 08:45):

@[simp] lemma one_mod_eq_one (n : ℕ) : 1 % (n + 2) = 1 :=
nat.mod_eq_of_lt (add_lt_add_right n.succ_pos 1)


#### Yakov Pechersky (Aug 14 2020 at 11:22):

#3763

Last updated: May 11 2021 at 13:22 UTC