# Questions tagged [natural-numbers]

For question about natural numbers $\Bbb N$, their properties and applications

12 questions
Filter by
Sorted by
Tagged with
97 views

### How to Prove Theorem le_zero in Lean4: If x ≤ 0, then x = 0?

I am playing the Natural Number Game found here and am trying to prove a theorem in Lean4. The theorem states that if a natural number x is less than or equal to 0, ...
• 141
113 views

### Proving that a minimum example exists if any example exists in nat

I'm trying to prove that if a function from nat -> bool is true for any natural number, then there exists a minimum natural number which the function is true for. I've been trying to find a good ...
44 views

### proof-based Pos type class

I'm working my way through the chapter on type classes in Functional Programming in Lean. The text demonstrates type-classes by representing positive numbers this way: ...
• 197
1 vote
58 views

### Injectivity, Surjectivity and Smallness on lists of natural numbers imply each other

Require Import Coq.Lists.List. I have the following properties defined on a list of natural numbers: ...
78 views

### Help with strong induction

I have the following definition of divisibility by 3. ...
1 vote
77 views

### Is every type-theoretic function ℕ → A extensionally equal to one written in terms of the ℕ-eliminator

In Category Theory the Natural Numbers object ℕ has the universal mapping-out property that tells us how to build arrows out of ℕ into an arbitrary object A. But it doesn't say that every arrow ...
• 345
409 views

### Using the contrapositive in lean 4

I'm trying to learn lean (version 4) by proving some basic facts about the natural numbers. Please feel free to critique my code if you see have general comments, but I also have a specific question ...
• 133
91 views

### How do I approach the final step in proving the cancellation law in Coq?

I'm trying to prove the cancellation law for natural numbers. This is my proof so far: ...
288 views

### Can you build W-types out of natural numbers predicatively?

I understand that we can use W-types to encode natural numbers and a wide variety of other inductive types in intensional MLTT. Can we encode W-types using only natural numbers within type theory, ...
• 517
143 views

### Proof by Exhaustive Computation for small initial segment of natural numbers (in Coq)

I have two functions f, g : nat -> nat. Let's pretend that f and g are cheap to compute. ...
1 vote
411 views

### Strong induction for nat in Coq

I'm doing some exercises on Coq and trying to prove the strong induction principle for nat: ...
• 195