Factorization by masahiro_sakai

module Theorem where

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

f : ∀ x a b → x * x + (a + b) * x + a * b ≡ (x + a) * (x + b)
f = solve 3 (λ x a b → x :* x :+ (a :+ b) :* x :+ a :* b := (x :+ a) :* (x :+ b)) refl