## Stream: Coq users

### Topic: ✔ How to prove a <= b -> a <= S b?

#### Daniel Hilst Selli (Dec 28 2021 at 15:43):

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.

#### Li-yao (Dec 28 2021 at 15:53):

Try to generalize the induction hypothesis (`generalize dependent` before `induction`).

#### Pierre Castéran (Dec 28 2021 at 16:54):

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

#### Daniel Hilst Selli (Dec 28 2021 at 23:31):

Thank you Pierre!

#### Notification Bot (Dec 28 2021 at 23:31):

Daniel Hilst Selli has marked this topic as resolved.

Last updated: Jan 29 2023 at 01:02 UTC