ne_zero without mul_zero_class

Stream: Is there code for X?

[Eric Rodriguez]

is there any (e.g. performance) reason that we state basic lemmas about no_zero_divisors with mul_zero_class as opposed to has_mul+has_zero? e.g. docs#mul_ne_zero:

import algebra.group_with_zero.basic

example {M} [has_mul M] [has_zero M] [no_zero_divisors M] (a b : M)
  (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 :=
mt eq_zero_or_eq_zero_of_mul_eq_zero $ not_or_distrib.mpr ⟨ha, hb⟩

[Junyan Xu]

Because the three lemmas above it, which share variables declarations with it, require that 0*m=m*0=0?

[Eric Rodriguez]

my question is essentially "is there any reason in practice we shouldn't change this" - sometimes I know there's shortcut lemmas for performance reasons, so I wonder if this needs to be one of them