## Stream: Coq users

### Topic: One less than other

#### zohaze (Sep 08 2022 at 15:50):

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

#### Emilio Jesús Gallego Arias (Sep 08 2022 at 15:55):

not likely, as if you replace `a` by `S b` in `a <= b` you get `S b <= b`

#### zohaze (Sep 08 2022 at 17:35):

``````S b > 0 ->
x = S a ->
a <= S b->
x <=b.
``````

a b x are nat

#### zohaze (Sep 09 2022 at 14:59):

Is above relation between two variables correct?

#### Mukesh Tiwari (Sep 09 2022 at 15:57):

@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.

#### Mukesh Tiwari (Sep 09 2022 at 15:59):

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.

#### zohaze (Sep 10 2022 at 04:27):

@Emilio Jesús Gallego Arias . Its means we can prove whole relation is false because S b <= b is wrong.

#### zohaze (Sep 10 2022 at 04:55):

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: Sep 23 2023 at 08:01 UTC