AB 3

Description

A special case of Euclid's lemma, which states that p | a * b → p ∣ a ⊎ p ∣ b when p is a prime number.

Theorem (download)

module Theorem where

open import Data.Nat
open import Data.Nat.Divisibility
open import Data.Sum

postulate
  ab3 : (a b : ℕ) → 3 ∣ a * b → 3 ∣ a ⊎ 3 ∣ b

Verifier

module Verifier where

open import Data.Nat
open import Data.Nat.Divisibility
open import Data.Sum
open import Theorem

verify : (a b : ℕ) → 3 ∣ a * b → 3 ∣ a ⊎ 3 ∣ b
verify = ab3

Proofs

Rank Prover Size Date
1 trigott 3991 2015-05-05 17:18:16 JST