Stream: Coq users

Topic: Is lia helpful here?


view this post on Zulip zohaze (Oct 12 2022 at 17:33):

S a <= S (S b)->
a < b

I am solving it with lia but unable to do it. How i can derive this?

view this post on Zulip Li-yao (Oct 12 2022 at 17:52):

Consider what happens if a and b are 0.

view this post on Zulip Pierre Rousselin (Oct 12 2022 at 19:17):

Li-Yao is right. The right lemma is :

Require Import Lia.
Theorem plop a b : S (S a) <= S b -> a < b.
Proof.  lia.  Qed.

which works (lia is wonderful).

view this post on Zulip zohaze (Oct 14 2022 at 17:23):

Ok, thanks.


Last updated: Feb 04 2023 at 21:02 UTC