Hi all,

I have the following example, not working:

Definition NatProp := forall (a b : nat), a > b → (a + 1) > (b + 1).

Lemma Test : forall (a b : nat), a > b → (a + 1) > (b + 1).

Proof. intros. apply NatProp. (* stuck *)

However, this works:

Axiom NatProp : forall (a b : nat), a > b → (a + 1) > (b + 1).

Lemma Test : forall (a b : nat), a > b → (a + 1) > (b + 1).

Proof. intros. apply NatProp. Qed.

This works too:

Lemma NatProp : forall (a b : nat), a > b → (a + 1) > (b + 1).

Proof. intros. lia. Qed.

Lemma Test : forall (a b : nat), a > b → (a + 1) > (b + 1).

Proof. intros. apply NatProp. exact H. Qed.

I’m still not really understanding how to kind of apply a definition in a proof, and did not find much when searching for this.

PS:because I am working with a system with multiple properties that I want to add as definitions to be used all along my proofs.

Thanks !

Lili

A definition is just a rename operation. If you want to use the definition of NatProp in a lemma, here’s how to do it.

```
From Coq Require Import Utf8.
Definition NatProp := forall (a b : nat), a > b → (a + 1) > (b + 1).
Lemma Test : NatProp.
Proof.
unfold NatProp.
intros.
Admitted.
```

An axiom is quite different. An axiom means “assume the following statement is true, without proof.”

In summary:

`Axiom Foo : ABC.`

“Assume the statement `ABC`

is true, without proof.”
`Theorem Foo : ABC.`

“The statement `ABC`

is true. I will give a proof of `ABC`

below.”
`Definition Foo := ABC.`

“The word `Foo`

is another name for `ABC`

.”

What is sometimes confusing is that definitions can have proofs. Such a situation arises when you are defining something and you need to prove that the object you are defining is well-defined. However, such usage is more advanced and you should learn the basics first before worrying about well-definedness.

1 Like

@davidjao please fix the typo: you put “:” intead of “:=” in Definition.

@Matafou Thanks for the correction! It should be noted that the `:`

notation is valid in the second case I mentioned, where a definition is followed by a proof.

```
Definition Foo : ABC.
Proof.
...
Defined.
```

But certainly this usage goes beyond the basics.

@davidjao As a novice who is lurking and learning, I appreciate the clarification.