Nat.div_one in the standard library

Stream: lean4

[Jad Ghalayini]

Hello! Do you guys think it would make sense to add

theorem div_one {n}: n / 1 = n := by {
  induction n with
  | zero => simp only [Nat.div_eq]
  | succ n I  => rw [Nat.div_eq, succ_sub_one, I]; simp_arith
}

to the standard library? It's missing from Div.lean for some reason, and it's a bit irritating to just have it hanging around in my project

[Leonardo de Moura]

@Jad Ghalayini We will be discussing the standard library (contributions, organization, etc) in the next dev update meeting this Thursday. For additional details:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/2nd.20Lean.20Dev.20Update.20Meeting