Could we convert a = S b into a <= b by le_S command?

not likely, as if you replace `a`

by `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