Could we convert a = S b into a <= b by le_S command?
not likely, as if you replace
S b in
a <= b you get
S b <= b
What about this relation
S b > 0 -> x = S a -> a <= S b-> x <=b.
a b x are nat
Is above relation between two variables correct?
@zohaze I am assuming you are working with natural numbers. We can assume b = 0 (S b = 1 > 0 holds), assume a = 0 (x = 1), a <= S b (0 <= 1 holds) but your goal x <= b (1 <= 0) does not hold and therefore, it's not provable.
Another way to think: you have assumed a <= S b and then you are trying to prove S a <= b (replace x by S a in the goal).
Ok, thank you.
@Emilio Jesús Gallego Arias . Its means we can prove whole relation is false because S b <= b is wrong.
1) From ( a<=S b) could we prove (a<=b) ? (Reverse of le_S.)
2) From ( a<=S b) could we prove (S a<= b) ?
Last updated: Feb 09 2023 at 00:03 UTC