H: a < b-> S (S a) < S b .

I have above hypothesis ,which is wrong (correct is a < b-> S (S a) <= S b . )

From H ,i want to derive contra statement. Is it possible?

Where do `a`

and `b`

come into scope? If they're already in scope before `H`

is introduced, then this is not a contradictory context, as `(a, b)`

could be `(0, 0)`

and `H`

could be by ex falso quodlibet.

Formally, if your context is:

```
a : nat
b : nat
H : a < b -> S (S a) < S b
```

then it's equivalent to the type `{ a : nat { b : nat & a < b -> S (S a) < S b } }`

, which can be inhabited:

```
Require Import Lia.
Goal { a : nat { b : nat & a < b -> S (S a) < S b } }.
exists 0.
exists 0.
lia.
Defined.
```

Yes, a & b :nat already in scope before H is introduced. Secondly, S a < S b exist in hypothesis and i have reduced them into a < b to make them simpl. Now i can say (0,0 ) could not be happen, a < b -> S (S a) < S b is not f alse statement and it could occur.

It’s difficult to help you if we don’t have a self-contained copy/pastable Coq script.

Coq is a formalism, and looking at an interactive proof attempt is more helpful than interpreting semi-formal statements like "happen", "occur".

Ok.

```
a : nat
b : nat
H : S a < S b -> S (S a) < S b
```

I want to ask that H statement may be prove False? (because correct is S a < S b -> S (S a) <= S b). Secondly,addition of another hypothesis a<=b may helpful. When run Lia command,i get message does not find witness. I just want to know , under what conditions H statement can be prove right or wrong ?

It's still equivalent to what you had before.

```
Require Import Lia.
Goal { a : nat { b : nat & S a < S b -> S (S a) < S b } }.
exists 0.
exists 0.
lia.
Defined.
```

It doesn't make sense to call `H`

"right" or "wrong". It is what it is, and true for certain values of `a`

and `b`

, and false for others. As an analogy, `a <= b`

is true for some values of `a`

and `b`

, and false for others. It's not "right" or "wrong".

If `H`

were true for all values of `a`

and `b`

, it'd be a useless hypothesis.

Last updated: Jan 31 2023 at 13:02 UTC