zohaze (Oct 12 2022 at 17:33): 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?
Li-yao (Oct 12 2022 at 17:52):Consider what happens if a and b are 0.
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).
zohaze (Oct 14 2022 at 17:23):Ok, thanks.
Last updated: Oct 01 2023 at 18:01 UTC