instMulPosMonoWithZeroOfMulRightMono

English

Instance giving MulPosMono for WithZero given Mul and order structure.

Русский

Экземпляр MulPosMono для WithZero с заданной умножением и порядком.

LaTeX

$$InstMulPosMonoWithZeroOfMulLeftMono$$

Lean4

instance {α : Type*} [Mul α] [Preorder α] [MulRightMono α] : MulPosMono (WithZero α) where
  elim :=
    @fun
      | ⟨0, _⟩, a, b, _ => by simp only [mul_zero, le_refl]
      | ⟨(x : α), _⟩, 0, _, _ => by simp only [zero_mul, WithZero.zero_le]
      | ⟨(x : α), _⟩, (a : α), 0, h => (lt_irrefl 0 (lt_of_lt_of_le (WithZero.zero_lt_coe a) h)).elim
      | ⟨(x : α), hx⟩, (a : α), (b : α), h => by
        dsimp only at h ⊢
        norm_cast at h ⊢
        exact mul_le_mul_right' h x

Похожие утверждения