    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some boring lemmas used by the ring solver
    ------------------------------------------------------------------------

    -- Note that these proofs use all "almost commutative ring" properties.

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

    open import Algebra using (RawRing)
    open import Algebra.Solver.Ring.AlmostCommutativeRing using (AlmostCommutativeRing; _-Raw-AlmostCommutative⟶_)

    module Algebra.Solver.Ring.Lemmas
      {r₁ r₂ r₃ r₄}
      (coeff : RawRing r₁ r₄)
      (r : AlmostCommutativeRing r₂ r₃)
      (morphism : coeff -Raw-AlmostCommutative⟶ r)
      where

    private
      module C = RawRing coeff
    open AlmostCommutativeRing r
    open import Algebra.Morphism
    open _-Raw-AlmostCommutative⟶_ morphism
    open import Relation.Binary.Reasoning.Setoid setoid
    open import Function.Base using (_⟨_⟩_; _$_)

    lemma₀ : ∀ a b c x →
             (a + b) * x + c ≈ a * x + (b * x + c)
    lemma₀ a b c x = begin
      (a + b) * x + c      ≈⟨ distribʳ _ _ _ ⟨ +-cong ⟩ refl ⟩
      (a * x + b * x) + c  ≈⟨ +-assoc _ _ _ ⟩
      a * x + (b * x + c)  ∎

    lemma₁ : ∀ a b c d x →
             (a + b) * x + (c + d) ≈ (a * x + c) + (b * x + d)
    lemma₁ a b c d x = begin
      (a + b) * x + (c + d)      ≈⟨ lemma₀ _ _ _ _ ⟩
      a * x + (b * x + (c + d))  ≈⟨ refl ⟨ +-cong ⟩ sym (+-assoc _ _ _) ⟩
      a * x + ((b * x + c) + d)  ≈⟨ refl ⟨ +-cong ⟩ (+-comm _ _ ⟨ +-cong ⟩ refl) ⟩
      a * x + ((c + b * x) + d)  ≈⟨ refl ⟨ +-cong ⟩ +-assoc _ _ _ ⟩
      a * x + (c + (b * x + d))  ≈⟨ sym $ +-assoc _ _ _ ⟩
      (a * x + c) + (b * x + d)  ∎

    lemma₂ : ∀ a b c x → a * c * x + b * c ≈ (a * x + b) * c
    lemma₂ a b c x = begin
      a * c * x + b * c  ≈⟨ lem ⟨ +-cong ⟩ refl ⟩
      a * x * c + b * c  ≈⟨ sym $ distribʳ _ _ _ ⟩
      (a * x + b) * c    ∎
      where
      lem = begin
        a * c * x    ≈⟨ *-assoc _ _ _ ⟩
        a * (c * x)  ≈⟨ refl ⟨ *-cong ⟩ *-comm _ _ ⟩
        a * (x * c)  ≈⟨ sym $ *-assoc _ _ _ ⟩
        a * x * c    ∎

    lemma₃ : ∀ a b c x → a * b * x + a * c ≈ a * (b * x + c)
    lemma₃ a b c x = begin
      a * b * x + a * c    ≈⟨ *-assoc _ _ _ ⟨ +-cong ⟩ refl ⟩
      a * (b * x) + a * c  ≈⟨ sym $ distribˡ _ _ _ ⟩
      a * (b * x + c)      ∎

    lemma₄ : ∀ a b c d x →
             (a * c * x + (a * d + b * c)) * x + b * d ≈
             (a * x + b) * (c * x + d)
    lemma₄ a b c d x = begin
      (a * c * x + (a * d + b * c)) * x + b * d              ≈⟨ distribʳ _ _ _ ⟨ +-cong ⟩ refl ⟩
      (a * c * x * x + (a * d + b * c) * x) + b * d          ≈⟨ refl ⟨ +-cong ⟩ ((refl ⟨ +-cong ⟩ refl) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ refl ⟩
      (a * c * x * x + (a * d + b * c) * x) + b * d          ≈⟨ +-assoc _ _ _  ⟩
      a * c * x * x + ((a * d + b * c) * x + b * d)          ≈⟨ lem₁ ⟨ +-cong ⟩ (lem₂ ⟨ +-cong ⟩ refl) ⟩
      a * x * (c * x) + (a * x * d + b * (c * x) + b * d)    ≈⟨ refl ⟨ +-cong ⟩ +-assoc _ _ _ ⟩
      a * x * (c * x) + (a * x * d + (b * (c * x) + b * d))  ≈⟨ sym $ +-assoc _ _ _ ⟩
      a * x * (c * x) + a * x * d + (b * (c * x) + b * d)    ≈⟨ sym $ distribˡ _ _ _ ⟨ +-cong ⟩ distribˡ _ _ _ ⟩
      a * x * (c * x + d) + b * (c * x + d)                  ≈⟨ sym $ distribʳ _ _ _ ⟩
      (a * x + b) * (c * x + d)                              ∎
      where
      lem₁′ = begin
        a * c * x    ≈⟨ *-assoc _ _ _ ⟩
        a * (c * x)  ≈⟨ refl ⟨ *-cong ⟩ *-comm _ _ ⟩
        a * (x * c)  ≈⟨ sym $ *-assoc _ _ _ ⟩
        a * x * c    ∎

      lem₁ = begin
        a * c * x * x    ≈⟨ lem₁′ ⟨ *-cong ⟩ refl ⟩
        a * x * c * x    ≈⟨ *-assoc _ _ _ ⟩
        a * x * (c * x)  ∎

      lem₂ = begin
        (a * d + b * c) * x        ≈⟨ distribʳ _ _ _ ⟩
        a * d * x + b * c * x      ≈⟨ *-assoc _ _ _ ⟨ +-cong ⟩ *-assoc _ _ _ ⟩
        a * (d * x) + b * (c * x)  ≈⟨ (refl ⟨ *-cong ⟩ *-comm _ _) ⟨ +-cong ⟩ refl ⟩
        a * (x * d) + b * (c * x)  ≈⟨ sym $ *-assoc _ _ _ ⟨ +-cong ⟩ refl ⟩
        a * x * d + b * (c * x)    ∎

    lemma₅ : ∀ x → (0# * x + 1#) * x + 0# ≈ x
    lemma₅ x = begin
      (0# * x + 1#) * x + 0#   ≈⟨ ((zeroˡ _ ⟨ +-cong ⟩ refl) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ refl ⟩
      (0# + 1#) * x + 0#       ≈⟨ (+-identityˡ _ ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ refl ⟩
      1# * x + 0#              ≈⟨ +-identityʳ _ ⟩
      1# * x                   ≈⟨ *-identityˡ _ ⟩
      x                        ∎

    lemma₆ : ∀ a x → 0# * x + a ≈ a
    lemma₆ a x = begin
      0# * x + a    ≈⟨ zeroˡ _ ⟨ +-cong ⟩ refl ⟩
      0# + a        ≈⟨ +-identityˡ _ ⟩
      a             ∎

    lemma₇ : ∀ x → - 1# * x ≈ - x
    lemma₇ x = begin
      - 1# * x      ≈⟨ -‿*-distribˡ _ _ ⟩
      - (1# * x)    ≈⟨ -‿cong (*-identityˡ _) ⟩
      - x           ∎