{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (CommutativeMonoid)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
module Algebra.Properties.CommutativeMonoid.Mult
{a ℓ} (M : CommutativeMonoid a ℓ) where
open CommutativeMonoid M
renaming
( _∙_ to _+_
; ∙-cong to +-cong
; ∙-congʳ to +-congʳ
; ∙-congˡ to +-congˡ
; identityˡ to +-identityˡ
; identityʳ to +-identityʳ
; assoc to +-assoc
; ε to 0#
)
open import Relation.Binary.Reasoning.Setoid setoid
open import Algebra.Properties.CommutativeSemigroup commutativeSemigroup
open import Algebra.Properties.Monoid.Mult monoid public
×-distrib-+ : ∀ x y n → n × (x + y) ≈ n × x + n × y
×-distrib-+ x y zero = sym (+-identityˡ 0# )
×-distrib-+ x y (suc n) = begin
x + y + n × (x + y) ≈⟨ +-congˡ (×-distrib-+ x y n) ⟩
x + y + (n × x + n × y) ≈⟨ +-assoc x y (n × x + n × y) ⟩
x + (y + (n × x + n × y)) ≈⟨ +-congˡ (x∙yz≈y∙xz y (n × x) (n × y)) ⟩
x + (n × x + suc n × y) ≈⟨ x∙yz≈xy∙z x (n × x) (suc n × y) ⟩
suc n × x + suc n × y ∎