The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

It has to do with the definition of < in the Coq standard library:

Definition lt (n m:nat) := S n <= m.

See https://coq.inria.fr/library/Coq.Arith.Lt.html

This means that a < b is *exactly defined to be* S a <= b, so the hypothesis H can be used as-is for the conclusion.

Best,

Cody

On Sun, Jul 12, 2015 at 6:59 PM, <yasu AT yasuaki.com> wrote:

Hi,

I am a beginner - why is the proof below ok?  I understand semantically this is trivial, but what is the mechanism of H to S a <= b  ?

Theorem T: forall a b:nat, a < b ->  S a <= b.
Proof .
    intros .
    exact H .
Qed.
Print T.

Cheers,

Yasuaki