Hi everybody, I posted the question on SO but ppl is voting for close as offtopic, so I'm comming directly here

I was trying to prove this lemma, which seems reasonable to be but I couldn't figure out how to do it

```
Lemma leb_0_r : forall x, x <=? 0 = true -> x = 0.
intros. induction x. reflexivity. discriminate H.
Qed.
Lemma leb_S : forall a b, a <=? b = true -> a <=? S b = true.
intros a b Hab. induction b. apply leb_0_r in Hab. now rewrite Hab.
```

But here I got stuck on the induction hypothesis

```
1 subgoal
a, b : nat
Hab : (a <=? S b) = true
IHb : (a <=? b) = true -> (a <=? S b) = true
========================= (1 / 1)
(a <=? S (S b)) = true
```

I tried induction on a too

```
Lemma leb_S : forall a b, a <=? b = true -> a <=? S b = true.
intros a b Hab. induction a. reflexivity. simpl. destruct b.
discriminate Hab. simpl in Hab.
1 subgoal
a, b : nat
Hab : (a <=? b) = true
IHa : (a <=? S b) = true -> (a <=? S (S b)) = true
========================= (1 / 1)
(a <=? S b) = true
```

The problem is that I always get to `S a <= b`

or `a <= S b`

and I can't simplify that.

Try to generalize the induction hypothesis (`generalize dependent`

before `induction`

).

You may try an induction on `a`

, before pushing `b`

in the context.

```
Lemma leb_S : forall a b, a <=? b = true -> a <=? S b = true.
induction a.
- cbn; reflexivity.
- destruct b.
+ discriminate.
+ cbn; intros; apply IHa; assumption.
Qed.
```

Thank you Pierre!

Daniel Hilst Selli has marked this topic as resolved.

Last updated: Oct 01 2023 at 18:01 UTC