Coq中证明乘法右分配律遇瓶颈，求基于已证定理的解法

我正在使用Coq 8.19.2证明《Software Foundations》中Induction章节的mult_plus_distr_r定理，定理表述为：

∀n m p : nat, (n + m) * p = (n * p) + (m * p)

目前已完成p=0的情况证明，但卡在子目标：

(n + m) * S p' = n * S p' + m * S p'

我清楚需要将(n + m) * S p'重写为(n + m) * p' + (n + m)，将n * S p' + m * S p'重写为n * p' + n + m * p' + m，但当前上下文没有对应的前提假设可以直接使用。我希望尽可能遵循教材内容，不使用auto等未介绍的命令或外部库。

以下是我已经证明完成的定理：

Theorem plus_O_n : forall n : nat, 0 + n = n.
Theorem plus_O_n' : forall n : nat, 0 + n = n.
Theorem plus_O_n'' : forall n : nat, 0 + n = n.
Theorem plus_1_l : forall n:nat, 1 + n = S n.
Theorem mult_0_l : forall n:nat, 0 * n = 0.
Theorem andb_commutative : forall b c, andb b c = andb c b.
Theorem andb_commutative' : forall b c, andb b c = andb c b.
Theorem lower_grade_F_Minus : lower_grade (Grade F Minus) = (Grade F Minus).
Theorem eqb_refle : forall n : nat, (eqb n n) = true.
Theorem mult_1_l : forall n:nat, 1 * n = n.
Theorem plus_id_exercise : forall n m o : nat,
  n = m -> m = o -> n + m = m + o.
Theorem mult_n_0_m_0 : forall p q : nat,
  (p * 0) + (q * 0) = 0.
Theorem mult_n_1 : forall p : nat,
  p * 1 = p.
Theorem plus_1_neq_0_firsttry : forall n : nat,
  (n + 1) =? 0 = false.
Theorem plus_1_neq_0 : forall n : nat,
  (n + 1) =? 0 = false.
Theorem negb_involutive : forall b : bool,
  negb (negb b) = b.
Theorem andb3_exchange :
  forall b c d, andb (andb b c) d = andb (andb b d) c.
Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Theorem plus_1_neq_0' : forall n : nat,
  (n + 1) =? 0 = false.
Theorem andb_commutative'' :
  forall b c, andb b c = andb c b.
Theorem zero_nbeq_plus_1 : forall n : nat,
  0 =? (n + 1) = false.
Theorem letter_comparison_Eq :
  forall l, letter_comparison l l = Eq.
Theorem lower_letter_lowers: forall (l : letter),
  letter_comparison (lower_letter l) l = Lt.
Theorem lower_letter_F_is_F:
  lower_letter F = F.
Theorem add_0_r_firsttry : forall n:nat,
  n + 0 = n.
Theorem add_0_r : forall n:nat,
  n + 0 = n.
Theorem mul_0_r : forall n:nat,
  n * 0 = 0.
Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Theorem add_comm : forall n m : nat,
  n + m = m + n.
Theorem add_assoc : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Theorem add_assoc2 : forall n m p : nat,
  n + (m + p) = n + m + p.
Theorem even_S : forall n : nat,
  even (S n) = negb (even n).
Theorem mult_0_plus' : forall n m : nat,
  (n + 0 + 0) * m = n * m.
Theorem plus_rearrange_firsttry : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Theorem plus_rearrange : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Theorem add_shuffle3 : forall n m p : nat,
  n + (m + p) = m + (n + p).
Theorem mult_0_r : forall n:nat,
  n * 0 = 0.
Theorem mul_comm : forall m n : nat,
  m * n = n * m.
Theorem plus_leb_compat_l : forall n m p : nat,
  n <=? m = true -> (p + n) <=? (p + m) = true.
Theorem leb_refl : forall n:nat,
  (n <=? n) = true.
Theorem zero_neqb_S : forall n:nat,
  0 =? (S n) = false.
Theorem andb_false_r : forall b : bool,
  andb b false = false.
Theorem S_neqb_0 : forall n:nat,
  (S n) =? 0 = false.
Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.
Theorem identity_fn_applied_twice :
  forall (f : bool -> bool),
  (forall (x : bool), f x = x) ->
  forall (b : bool), f (f b) = b.
Theorem negation_fn_applied_twice  :
  forall (f : bool -> bool),
  (forall (x : bool), f x = negb x) ->
  forall (b : bool), f (f b) = b.
Theorem andb_eq_orb :
  forall (b c : bool),
  (andb b c = orb b c) ->
  b = c.
Theorem all3_spec : forall b c : bool,
  orb
    (andb b c)
    (orb (negb b)
         (negb c))
  = true.

我正在梳理这些已证定理，思考如何通过重写或调整归纳假设推进证明，目前认为归纳假设是正确的。

内容的提问来源于stack exchange，提问作者user18476546