Lemma. Multiply 0 is 0 [ring-0002]

module ring-0002 where

open import MLTT.Spartan

open import ring-0000
open Ring {{...}}

lemma-1 : {R : 𝓤 ̇ } {{_ : Ring R}} → (r : R) → (r ⊗ 𝟘R ＝ 𝟘R) × (𝟘R ⊗ r ＝ 𝟘R)
lemma-1 r = (ring-cancel-right I ⁻¹) , (ring-cancel-right II ⁻¹)
  where
  I : 𝟘R ⊕ r ⊗ 𝟘R ＝ r ⊗ 𝟘R ⊕ r ⊗ 𝟘R
  I =
    𝟘R ⊕ r ⊗ 𝟘R   ＝⟨ 0l-neu (r ⊗ 𝟘R) ⟩
    r ⊗ 𝟘R        ＝⟨ ap (r ⊗_) (0l-neu 𝟘R ⁻¹) ⟩
    r ⊗ (𝟘R ⊕ 𝟘R) ＝⟨ distrib2 ⟩
    r ⊗ 𝟘R ⊕ r ⊗ 𝟘R ∎

  II : 𝟘R ⊕ 𝟘R ⊗ r ＝ 𝟘R ⊗ r ⊕ 𝟘R ⊗ r
  II =
    𝟘R ⊕ 𝟘R ⊗ r   ＝⟨ 0l-neu (𝟘R ⊗ r) ⟩
    𝟘R ⊗ r        ＝⟨ ap (_⊗ r) (0l-neu 𝟘R ⁻¹) ⟩
    (𝟘R ⊕ 𝟘R) ⊗ r ＝⟨ distrib1 ⟩
    𝟘R ⊗ r ⊕ 𝟘R ⊗ r ∎