```
(a <= k) ->
((S a) <= k) ->
(a <= S k) .
```

If first two relations hold then we can prove third one? Secondly,below statement is contra statement?

```
(1 <= k)
(0 <= S k)
```

zohaze said:

`(a <= k) -> ((S a) <= k) -> (a <= S k) .`

If first two relations hold then we can prove third one?

You only need the first relation to prove the third.

What about second part of question?

Seems like `k = 1`

satisfies both `1 <= k`

and `0 <= S k`

..

From above three relation , can i say a > 0 or a <> 0?

Well, `a = 0`

and `k = 1`

satisfies all three.. could I ask why you are asking these questions?

In hypothesis i have a=0 and want to check H is true or false. May be it is contra statement. I am looking for some contra statement in all above.

Contradiction you are seeking here does not exist. I feel like this is XY problem, could you show the whole of what you are doing?

I have sub goal statement = False. There is no other hypothesis above 3 and a=0. Want to complete it.

That still does not sound like the whole thing. Why are you doing that, what do you ultimately want to prove?

Just to prove above combination is not possible.

I mean, there must be a reason you are proving this somewhat arbitrary proposition. (Which I believe is not true, after all)

```
between_le: forall (P : nat -> Prop) (k l : nat), between P k l -> k <= l
exists_le_S: forall (Q : nat -> Prop) (k l : nat), exists_between Q k l -> S k <= l
```

By using above , could i prove below one

```
H: a <= k
Goal: S a <=k
```

No, and the counterexample is any case where a = k (say, both are 0).

If you get to this goal from a valid theorem, then you have chosen the wrong proof strategy.

So, @abab9579 is 100% right. We cannot help you solve your task with the questions you're asking.

If above is not true then we can prove it False? Secondly, what maximum information we can extract from below (especially S a=0 or S a=1)

```
H: a <= k
H1: S a <= k
H2: a <= S k
```

For the first question: whether the implication ` (a <= k -> S a <= k)`

is true or false depends on `a`

and `k`

. But you didn't give any information about these variables. As several of us already mentionned, we cannot help to solve sub-goals which are too partially presented; the best being a script we can replay without having to guess and re-type the missing information.

The following three lemmas clearly show that this implication is sometimes false, sometimes true.

```
Require Import Arith Lia.
Lemma L : ~ forall a k, (a <= k -> S a <= k).
Proof. intro H . specialize (H 0 0). lia. Qed.
Lemma L': exists a k, ~ (a <= k -> S a <= k).
Proof. exists 0, 0; lia. Qed.
Lemma L'' : exists a k, (a <= k -> S a <= k).
Proof. exists 0, 42; lia. Qed.
```

For the second question, the conjunction of your three propositions is clearly equivalent to `a < k`

.

```
Goal forall a k, (a <= k /\ S a <= k /\ a <= S k) <-> a < k.
Proof. lia. Qed.
```

Thank you. a & k are natural numbers. Therefore they can be zero or non zero. Should i consider both cases separately?

If what you're trying to prove is not true, no proof strategy will help.

Ok, thanks to all of you.

```
H1: S a <= k
H2: a <= S k
H3: S k >0
```

From above could i write (S a=k) or (a=k) or what other information may extract?

`H3`

is redundant: You could prove it for any `k`

because a successor is always greater than 0. `H1`

implies `H2`

: From `S a <= k`

we get `S a <= S k`

and `S a <= S (S k)`

by applying `le_S`

twice. Then, `le_S_n`

gives us `a <= S k`

. So, in summary, all you know is that `S a <= k`

.

Last updated: Jun 25 2024 at 18:02 UTC