instPosMulMonoWithZeroOfMulLeftMono

English

Instance giving PosMulMono for WithZero from MulLeftMono.

Русский

Экземпляр PosMulMono для WithZero от MulLeftMono.

LaTeX

$$InstPosMulMonoWithZeroOfMulLeftMono$$

Lean4

instance {α : Type*} [Mul α] [Preorder α] [MulLeftMono α] : PosMulMono (WithZero α) where
  elim :=
    @fun
      | ⟨0, _⟩, a, b, _ => by simp only [zero_mul, le_refl]
      | ⟨(x : α), _⟩, 0, _, _ => by simp only [mul_zero, 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_left' h x

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