Commit 2019-09-16 23:07 dd0ff1c4

feat(data/nat/basic): dvd_add_self_{left,right} (#1448)

• feat(data/nat/basic): dvd_add_self_{left,right} Two simp-lemmas of the form

@[simp] protected lemma dvd_add_self_left {m n : ℕ} :
  m ∣ m + n ↔ m ∣ n :=
dvd_add_right (dvd_refl m)

• Oops, lemmas were protected
• Provide version for rings