S a <= S (S b)-> a < b
I am solving it with lia but unable to do it. How i can derive this?
Consider what happens if
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).
Last updated: Feb 04 2023 at 21:02 UTC