mathlib3

292e3fa1 - refactor(nat/basic): Move lemma about nat (#8539)