mathlib

d936c288 - feat(data/real/nnreal): coe_max and coe_min (#2346)