mathlib

6ca08e81 - feat(algebra/ne_zero): add `coe_trans` instance (#11700)

feat(algebra/ne_zero): add `coe_trans` instance (#11700) This is super-useful for `flt_regular`, meaning we don't have to write all of our lemmata as `ne_zero ((n : ℕ) : R)`.