Commit 2020-06-30 03:05 056a72aa

perf(linarith): don't repeat nonneg proofs for nat-to-int casts (#3226) This performance issue showed up particularly when using nlinarith over nats. Proofs that (n : int) >= 0 were being repeated many times, which led to quadratic blowup in the nlinarith preprocessing.