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

Question

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 *)
        simpl. rewrite -> add_0_r_firsttry. 
        rewrite -> n_le_sum_n_m. reflexivity.
    - (* n = S n' *)
        induction p as [| p' IHp' ].
        -- (* p = 0 *)
            rewrite -> add_comm, add_0_r_firsttry, add_comm, add_0_r_firsttry.
            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?

Answer 1

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.

Answer 2

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

Answer 3

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.