Can someone help me with this proof about the pumping lemma using coq?

Question

This is an exercise from software foundation.

I have proved weak pumping lemma, but I don't know how the prove the strong one. When I try proving the third case 'App', I can't deal with length (s1 ++ s3) + length s4 <= pumping_constant re1 + pumping_constant re2.

These are my previous proof.

Lemma pumping: forall T (re: reg_exp T) s,
  s =~ re ->
  pumping_constant re <= length s ->
  exists s1 s2 s3,
    s = s1 ++ s2 ++ s3 /\
    s2 <> [] /\
    length s1 + length s2 <= pumping_constant re /\
    forall m, s1 ++ napp m s2 ++ s3 =~ re.
Proof.
  intros T re s Hmatch.
  induction Hmatch.
  - simpl. intros contra. inversion contra.
  - simpl. intros contra. inversion contra. inversion H0.
  - simpl. intros H. rewrite app_length in H. apply add_le_cases in H. destruct H.
    + destruct (IHHmatch1 H) as [s3 [s4 [s5 [H1 [H2 [H3 H4]]]]]].
      exists s3. exists s4. exists (s5 ++ s2). split.
      {
        rewrite H1. rewrite (app_assoc _ s3 s4 s5). 
        rewrite <- (app_assoc _ (s3 ++ s4) s5 s2). rewrite <- (app_assoc _ s3 s4 (s5 ++ s2)). 
        reflexivity.
      } split.
      { apply H2. } split.
      { apply le_trans with (n := pumping_constant re1). apply H3. apply le_plus_l. }
      {
        intros m.
        rewrite app_assoc. rewrite app_assoc. rewrite <- (app_assoc _ s3 _ s5).
        apply MApp. apply H4. apply Hmatch2.
      }
    + destruct (IHHmatch2 H) as [s3 [s4 [s5 [H1 [H2 [H3 H4]]]]]].
      exists (s1 ++ s3). exists s4. exists s5. split.
      {
        rewrite H1. rewrite (app_assoc _ s3 s4 s5). 
        rewrite app_assoc. rewrite (app_assoc _ s1 s3 s4). rewrite <- app_assoc.
        reflexivity.
      } split.
      { apply H2. } split.
      {  }