lemmas related to core

Stream: new members

[Yakov Pechersky]

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]

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

[Chris Wong]

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

[Chris Wong]

@[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]

#3763