The Coq mailing list

[yasu AT yasuaki.com]

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