Factorization by Lost_dog_

module Theorem where

open import Data.Nat
open import Relation.Binary.PropositionalEquality as P
open import Data.Nat.Properties
open import Data.Product
import Algebra as A
open A.CommutativeSemiring commutativeSemiring hiding (_+_;_*_;sym)
open P.≡-Reasoning

f : ∀ x a b → x * x + (a + b) * x + a * b ≡ (x + a) * (x + b)
f x a b with 
  begin 
    (x + a) * (x + b)
  ≡⟨ proj₂ distrib (x + b) x a ⟩
    x * (x + b) + a * (x + b)
  ≡⟨ cong (λ e → e + a * (x + b)) (proj₁ distrib x x b) ⟩
    x * x + x * b + a * (x + b)
  ≡⟨ cong (λ e → x * x + x * b + e) (proj₁ distrib a x b) ⟩
    x * x + x * b + (a * x + a * b)
  ≡⟨ +-assoc (x * x) (x * b) (a * x + a * b) ⟩
    x * x + (x * b + (a * x + a * b))
  ≡⟨ cong (λ e → x * x + e) (sym (+-assoc (x * b) (a * x) (a * b))) ⟩
    x * x + ((x * b + a * x) + a * b)
  ≡⟨ cong (λ e → x * x + ((e + a * x) + a * b)) (*-comm x b) ⟩
    x * x + ((b * x + a * x) + a * b)
  ≡⟨ cong (λ e → x * x + (e + a * b)) (+-comm (b * x) (a * x)) ⟩
    x * x + ((a * x + b * x) + a * b)
  ≡⟨ cong (λ e → x * x + (e + a * b)) (sym (proj₂ distrib x a b)) ⟩
    x * x + (((a + b) * x) + a * b)
  ≡⟨ sym (+-assoc (x * x) ((a + b) * x) (a * b)) ⟩
    x * x + (a + b) * x + a * b
  ∎
...| z = sym z