```------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of semimodules.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra                using (CommutativeSemiring)
open import Algebra.Module.Bundles using (Semimodule)
open import Level                  using (Level)

module Algebra.Module.Properties.Semimodule
{r ℓr m ℓm : Level}
{semiring  : CommutativeSemiring r ℓr}
(semimod   : Semimodule semiring m ℓm)
where

open CommutativeSemiring semiring
open Semimodule          semimod
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid

x≈0⇒x*y≈0 : ∀ {x y} → x ≈ 0# → x *ₗ y ≈ᴹ 0ᴹ
x≈0⇒x*y≈0 {x} {y} x≈0 = begin
x  *ₗ y ≈⟨ *ₗ-congʳ x≈0 ⟩
0# *ₗ y ≈⟨ *ₗ-zeroˡ y ⟩
0ᴹ      ∎

y≈0⇒x*y≈0 : ∀ {x y} → y ≈ᴹ 0ᴹ → x *ₗ y ≈ᴹ 0ᴹ
y≈0⇒x*y≈0 {x} {y} y≈0 = begin
x *ₗ y  ≈⟨ *ₗ-congˡ y≈0 ⟩
x *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ x ⟩
0ᴹ      ∎

x*y≉0⇒x≉0 : ∀ {x y} → x *ₗ y ≉ᴹ 0ᴹ → x ≉ 0#
x*y≉0⇒x≉0 = contraposition x≈0⇒x*y≈0

x*y≉0⇒y≉0 : ∀ {x y} → x *ₗ y ≉ᴹ 0ᴹ → y ≉ᴹ 0ᴹ
x*y≉0⇒y≉0 = contraposition y≈0⇒x*y≈0
```