当 Coq 无法将我的目标与 IH 统一时，我该如何重写或使用 IH？

我正在尝试证明一个插入基于列表的优先级队列的正确性定理。以下是插入函数、归纳性质以及我正在使用的证明：

Fixpoint insert (x : nat) (l : list nat) : list nat :=
  match l with
  | [] => [x]
  | h :: t => if x <=? h then x :: h :: t else h :: insert x t
  end.

Inductive list_PQ_property : list nat -> Prop :=
| sorted_empty : list_PQ_property []
| sorted_one : forall x, list_PQ_property [x]
| sorted_add : forall x y l,
    x <= y ->
    list_PQ_property (y :: l) ->
    list_PQ_property (x :: y :: l).

Theorem insert_correctness :
  forall (pq : PQ) (x : el),
    list_PQ_property pq ->
    list_PQ_property (insert x pq).
Proof.
  intros pq x H.
  induction H as [ | y | a b l Hab IHl].
  - simpl. apply sorted_one.
  - simpl. destruct (x <=? y) eqn:E.
    + apply Nat.leb_le in E. apply sorted_add.
      * apply E.
      * apply sorted_one.
    + apply Nat.leb_gt in E.
      apply Nat.lt_le_incl in E.
      apply sorted_add.
      * apply E.
      * apply sorted_one.
  - simpl. destruct (x <=? a) eqn:E.
    + apply Nat.leb_le in E.
      apply sorted_add.
      * apply E.
      * apply sorted_add.
        -- apply Hab.
        -- apply IHl.
  + destruct (x <=? b) eqn:E'.
      * apply Nat.leb_le in E'.
      apply sorted_add.
      apply Nat.lt_le_incl.
      apply Nat.leb_gt in E. apply E.
      apply sorted_add.
        ++ apply E'.
        ++ apply IHl.
       * apply Nat.leb_gt in E'.
        apply sorted_add.
        -- apply Hab.
Admitted.

当我开始证明的时候，一切都很简单，直到我遇到第三个情况。一开始我卡在了

apply sorted_add.
        ++ apply E'.
        ++ apply IHl.

我的目标是 ，b <= x但我对 E' 的假设是 ，x <= b直到我通过应用 Coq 中的一堆 Nat 函数绕过了传递性。现在我卡在了 ，我的 IHIHl 假设如下所示： IHIHl : list_PQ_property (insert x (b :: l)) ，但我的目标是： list_PQ_property (b :: insert x l)。

我不知道如何解决这个问题，或者我是否正确地证明了这一点。

任何指导都将不胜感激。

欲了解更多信息，到目前为止我的完整目标是这样的：

1 goal
x : el
a, b : nat
l : list nat
Hab : a <= b
IHl : list_PQ_property (b :: l)
IHIHl : list_PQ_property (insert x (b :: l))
E : (x <=? a) = false
E' : b < x
______________________________________(1/1)
list_PQ_property (b :: insert x l)

我试过用 IHIHl，但没用。我有点迷茫，我猜这就是我建立证明的方法。