Coq中Program Fixpoint的diff函数剩余证明义务求解

我正在用Coq实现一个名为diff的函数，用于对算术表达式e关于变量x求导。相关代码定义如下：

Inductive aexp : Type :=
| Const : Z -> aexp
| Var : string -> aexp
| Power : string -> Z -> aexp
| Times : list aexp -> aexp
| Sum : list aexp -> aexp.

Fixpoint rank (e:aexp) : nat :=
    match e with
    | Const n => 1
    | Var a => 1
    | Power a n => 1
    | Times l => 1 + (fix sum_rank l :=
                        match l with
                        | [] => 0
                        | hd :: tl => (rank hd) + (sum_rank tl)
                        end) l
    | Sum l => 1 + (fix sum_rank l :=
                        match l with
                        | [] => 0
                        | hd :: tl => (rank hd) + (sum_rank tl)
                        end) l
    end.

Program Fixpoint diff (e:aexp) (x:string) {measure (rank e)} : aexp :=
    match e with
    | Const n => Const 0
    | Var a => (if negb (String.eqb a x) then Const 0 else Const 1)
    | Power a n => (if Z.ltb n  0 then Var "ERROR"
                    else if (Z.eqb n  0) || negb (String.eqb a x) then Const 0
                    else Times [Const n; (Power a (n-1))])
    | Times l => (match l with
                | [] => Var "ERROR"
                | [hd] => diff hd x
                | hd ::tl => Sum [Times ((diff hd x)::tl); Times [hd; diff (Times tl) x]]
    end)
    |Sum l => (match l with
            | [] => Var "ERROR"
            (* | _ => Sum (map (fun e => diff e x) l x) *)
            | _ => Sum (map (fun e => diff e x) l)
            end)
    end.

目前我已经完成了3项证明义务，但仍有2项未解决。当前卡在证明**当e是l的元素时，rank e < rank (Sum l)**这一步，当前上下文的命题如下：

x : string
l : list aexp
diff : forall e : aexp, string -> rank e < rank (Sum l) -> aexp
n : [] <> l
e : aexp

核心疑问：如何从上述命题中推出e属于l的事实？

以下是我已完成的3项证明义务代码供参考：

Next Obligation.
Proof.
    simpl.
    rewrite Nat.add_0_r.
    apply Nat.lt_succ_diag_r.
    Qed.
Next Obligation.
Proof.
    simpl.
    rewrite <- Nat.add_succ_r .
    Search (_ < _ + _).    
    rewrite <- Nat.add_0_r at 1.
    rewrite <- Nat.add_lt_mono_l with (p := rank hd).
    assert (forall n, 0 < S n).
    {
        induction n0.
        firstorder.
        firstorder.
    }
    apply H.
Qed.
Next Obligation.
Proof.
    simpl.
    assert (forall e, rank e > 0).
    {
        induction e.
        simpl.
        firstorder.
        simpl.
        firstorder.
        simpl.
        firstorder.
        simpl.
        assert (forall n, 0 < S n).
        {
            induction n0.
            firstorder.
            firstorder.
        }
        apply H.
        simpl.
        assert (forall n, 0 < S n).
        {
            induction n0.
            firstorder.
            firstorder.
        }
        apply H.
    }
    rewrite <- Nat.add_succ_r.
    Search ( _ + _  = _ + _).
    rewrite Nat.add_comm.
    rewrite <- Nat.add_0_r at 1.
    rewrite <- Nat.add_lt_mono_l.
    apply H.
    Qed.

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