Factorization by trigott

module Theorem where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

open import Data.Nat.Properties

open import Algebra
import Data.Nat.Properties as Nat
private
  module CS = CommutativeSemiring Nat.commutativeSemiring

open import Data.Product

-- x * x + (a + b) * x + a * b
-- x * x + (a * x + b * x) + a * b
-- (x * x + a * x) + b * x + a * b
-- (x * x + a * x) + (b * x + a * b)
-- (x * x + a * x) + (x * b + a * b)
-- (x + a) * x   + (x + a) * b
-- (x + a) * (x + b)

f : ∀ x a b → x * x + (a + b) * x + a * b ≡ (x + a) * (x + b)
f x a b =
    trans (cong (λ p → x * x + p + a * b) ((proj₂ CS.distrib) x a b))
          (trans (cong (λ p → p + a * b) (sym (CS.+-assoc (x * x) (a * x) (b * x))))
                 (trans (CS.+-assoc (x * x + a * x) (b * x) (a * b))
                        (trans (cong (λ p → x * x + a * x + (p + a * b)) (CS.*-comm b x))
                               (trans (cong₂ _+_ (sym ((proj₂ CS.distrib) x x a))
                                                 (sym ((proj₂ CS.distrib) b x a)))
                                      (sym ((proj₁ CS.distrib) (x + a) x b))))))