data.nat.basic mathlib3#729

Stream: mathlib4

[Scott Morrison]

mathlib4#729, porting data.nat.basic, should be a priority. It has some annoying obstacles. One is even_odd_rec which is a wrapper around binary_rec that we haven't ported. As this isn't actually used anywhere in mathlib, I propose we punt on this.

#17759 moves it out to its own file.

[Scott Morrison]

And #17763 moves more material about bit out of data.nat.basic. If this could also be approved quickly that would be great, so we can resume porting data.nat.basic.

[Scott Morrison]

Besides the question in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/elab_as_elim/near/312963332 and getting #17763 approved, I think we are ready to merge Data.Nat.Basic now.