mathlib3

056a72aa - perf(linarith): don't repeat nonneg proofs for nat-to-int casts (#3226)

perf(linarith): don't repeat nonneg proofs for nat-to-int casts (#3226) This performance issue showed up particularly when using `nlinarith` over `nat`s. Proofs that `(n : int) >= 0` were being repeated many times, which led to quadratic blowup in the `nlinarith` preprocessing. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>