An instance orphaned from Algebra.Order.Monoid.WithZero.Defs #
We put this here to minimise imports: if you can move it back into
Algebra.Order.Monoid.WithZero.Defs without increasing imports, please do.
instance
WithZero.contravariantClass_mul_lt
{α : Type u}
[Mul α]
[PartialOrder α]
[ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
:
ContravariantClass (WithZero α) (WithZero α) (fun x x_1 => x * x_1) fun x x_1 => x < x_1