How can I rewrite or use my IH when Coq won't unify my goal with it?

Im trying to prove a correctness theorem for insert into a list-based priority queue. Here's the insert function, the inductive property, and the proof I'm working with:

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.

When I started the proof everything was straightforward until I got to the third case. At first I was getting stuck at the

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

in which my goal was b <= x but my hypothesis for E' was x <= b until I bypassed the transitivity properties by apply a bunch of Nat functions found in Coq. Now I'm stuck at in where my IHIHl hypothesis looks like this: IHIHl : list_PQ_property (insert x (b :: l)) but my goal is this: list_PQ_property (b :: insert x l).

I'm not sure how to fix this or if I am even proving this correctly.

Any guidance will be appreciated.

For more info my full goal looks like this so far:

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)

I tried using IHIHl as it was to no avail. I am a little lost as I am guessing its how I built my proof.

insert x (b :: l) reduces to if x <=? b then x :: b :: l else b :: insert x l, which is not b :: insert x l. You can simplify IHIHl to make the latter term appear, get a proof that x <=? b = false from E' : b < x and rewrite this proof in IHIHl to make the term reduce further.