mathlib

6e6e6da6 - feat(data/nat/basic): two identities for `choose` (#1936)

feat(data/nat/basic): two identities for `choose` (#1936) * feat(data/nat/basic): two identities for `choose` * fix build Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>