# Making use of a definition inside a proof

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.
``````

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.