Factorization

Description

Exercise for deformation of natural numbers.

Theorem (download)

module Theorem where

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

postulate
  f : ∀ x a b → x * x + (a + b) * x + a * b ≡ (x + a) * (x + b)

Verifier

module Verifier where

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

verify : ∀ x a b → x * x + (a + b) * x + a * b ≡ (x + a) * (x + b)
verify = f

Proofs

Rank Prover Size Date
1 notogawa 220 2013-08-29 23:41:03 JST
2 masahiro_sakai 240 2014-11-30 22:37:33 JST
3 trigott 693 2014-04-15 23:55:35 JST
4 Lost_dog_ 791 2013-08-29 17:52:51 JST