agda-extras

Some extra stuff to supplement agda-stdlib (v1.3).

Theories

Currently has some additional theories on Nat in src/Extra/Data/Nat, including

Factorials _! (in Factorial.agda)
- m≤n⇒m!∣n! : _! Preserves _≤_ ⟶ _∣_
Binomial coefficients _C_ (in Binomial.agda)
- C-!-div : ∀ (m n : ℕ) → (m + n) C m ≡ ((m + n) !) / (m ! * n !)
- C-!-mod : ∀ (m n : ℕ) → ((m + n) !) % (m ! * n !) ≡ 0
Fibonacci numbers fib (in Fibonacci.agda)
- fib-rec : ∀ (m n : ℕ) → fib (suc (m + n)) ≡ fib m * fib n + fib (suc m) * fib (suc n)
- fib-gcd-suc : ∀ n → gcd (fib n) (fib (suc n)) ≡ 1
- fib-gcd : ∀ (m n : ℕ) → gcd (fib m) (fib n) ≡ fib (gcd m n)
GCD (in GCD.agda)
- gcd[n,0]≡n : ∀ n → gcd n 0 ≡ n
- gcd-split : ∀ m n d → Coprime m n → d ∣ m * n → d ≡ gcd d m * gcd d n
- gcd-multʳ : ∀ k → Multiplicative (gcd k)
- gcd-induction : ∀ {P : ℕ → ℕ → Set} (m n : ℕ) → (∀ m → P m 0) → (∀ m n {≢0} → P n ((m % n) {≢0}) → P m n) → P m n
Primes (in Prime.agda)
- Definition of Composite
- composite-div : ∀ {n} → Composite n → ∃[ d ] (1 < d × d < n × d ∣ n)
- ∃p∣n : ∀ {n} → n > 1 → ∃[ p ] (Prime p × p ∣ n)
- Infinitude of primes: inf-primes : Inf Prime