Scott Fleischman scott-fleischman

copumpkin / Prime.agda

Last active December 25, 2023 19:01

There are infinite primes

	module Prime where

	open import Coinduction

	open import Data.Empty
	open import Data.Nat
	open import Data.Nat.Properties
	open import Data.Nat.Divisibility
	open import Data.Fin hiding (pred; _+_; _<_; _≤_; compare)
	open import Data.Fin.Props hiding (_≟_)