open import Algebra
module Algebra.Props.Ring (r : Ring) where
open Ring r
import Relation.Binary.EqReasoning as EqR; open EqR setoid
open import Data.Function
open import Data.Product
-‿*-distribˡ : ∀ x y → - x * y ≈ - (x * y)
-‿*-distribˡ x y = begin
- x * y ≈⟨ sym $ proj₂ +-identity _ ⟩
- x * y + 0# ≈⟨ refl ⟨ +-pres-≈ ⟩ sym (proj₂ -‿inverse _) ⟩
- x * y + (x * y + - (x * y)) ≈⟨ sym $ +-assoc _ _ _ ⟩
- x * y + x * y + - (x * y) ≈⟨ sym (proj₂ distrib _ _ _) ⟨ +-pres-≈ ⟩ refl ⟩
(- x + x) * y + - (x * y) ≈⟨ (proj₁ -‿inverse _ ⟨ *-pres-≈ ⟩ refl)
⟨ +-pres-≈ ⟩
refl ⟩
0# * y + - (x * y) ≈⟨ proj₁ zero _ ⟨ +-pres-≈ ⟩ refl ⟩
0# + - (x * y) ≈⟨ proj₁ +-identity _ ⟩
- (x * y) ∎
-‿*-distribʳ : ∀ x y → x * - y ≈ - (x * y)
-‿*-distribʳ x y = begin
x * - y ≈⟨ sym $ proj₁ +-identity _ ⟩
0# + x * - y ≈⟨ sym (proj₁ -‿inverse _) ⟨ +-pres-≈ ⟩ refl ⟩
- (x * y) + x * y + x * - y ≈⟨ +-assoc _ _ _ ⟩
- (x * y) + (x * y + x * - y) ≈⟨ refl ⟨ +-pres-≈ ⟩ sym (proj₁ distrib _ _ _) ⟩
- (x * y) + x * (y + - y) ≈⟨ refl ⟨ +-pres-≈ ⟩ (refl ⟨ *-pres-≈ ⟩ proj₂ -‿inverse _) ⟩
- (x * y) + x * 0# ≈⟨ refl ⟨ +-pres-≈ ⟩ proj₂ zero _ ⟩
- (x * y) + 0# ≈⟨ proj₂ +-identity _ ⟩
- (x * y) ∎