The Coq mailing list

[yasu AT yasuaki.com]

Hi Cody,  I see. this makes sense.  Thank you! :-) Cheers,Yasu

On 13.07.2015 08:26, roux cody wrote:
> 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 [1]
> 
> 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
> 
> 
> 
> Links:
> ------
> [1] https://coq.inria.fr/library/Coq.Arith.Lt.html