# How do I approach the final inductive step in plus_leb_compat_l from Software Foundations?

I'm provided with this theorem from the Software Foundations textbook:

Theorem plus_leb_compat_l : forall n m p : nat,
n <=? m = true -> (p + n) <=? (p + m) = true.


Pretty simple proof up until the second step in the nested inductive step. This is my work so far:

Theorem plus_leb_compat_l : forall n m p : nat,
n <=? m = true -> (p + n) <=? (p + m) = true.
Proof.
intros n m p H. induction n as [| n' IHn' ].
- (* n = 0 *)
rewrite -> n_le_sum_n_m. reflexivity.
- (* n = S n' *)
induction p as [| p' IHp' ].
-- (* p = 0 *)
rewrite -> H. reflexivity.
-- (* p = S n' *)
simpl.


I end up with the hypothesis (p' + S n' <=? p' + m) = true, which I don't think can be proven true for arbitrary n' and m, as n' is any arbitrary nonnegative, and m is any natural number. I think I could perform an inductive proof on m, but I'm unsure that would be fruitful.

The textbook provides the hint "If a hypothesis has the form H: P -> a = b, then rewrite H will rewrite a to b in the goal, and add P as a new subgoal. Use that in the inductive step of this exercise." This doesn't seem too helpful, is there anything clear that I'm missing?

Induction on p, as Pierre Jouvelot suggests, makes this proof much easier (the challenge is recognising it but it will come with experience).

Theorem plus_leb_compat_l : forall n m p : nat,
n <=? m = true -> (p + n) <=? (p + m) = true.
Proof.
intros ? ? ?.
revert m;
revert n.
induction p as [|p IHp];
simpl.
+
intros ? ? Ha;
exact Ha.
+
intros ? ? Ha;
eapply IHp;
exact Ha.
Qed.

• Induction on p worked! Thank you! Dec 27, 2022 at 15:05

You could try to do the induction on p instead of n.

• This worked, thank you! Dec 27, 2022 at 15:05

Indeed, there is no need to use explicit rewriting. The reductions of leb (S n) (S m)to leb n m and S n + m to S (n+m) suggest a simple proof by induction on p.

Lemma L:
forall n m p : nat, (n <=? m) = true -> (p + n <=? p + m) = true.
Proof.
induction p; simpl.
- now intros ?.
- assumption.
Qed.