conv => 
  rhs
  rw [Nat.add_assoc]
  conv => 
    rhs
    rw [← Nat.add_assoc]
    conv => 
      lhs
      rw [Nat.add_comm]  
    rw [Nat.add_assoc]
    simp [Nat.add]
  rw [←Nat.add_assoc]
ys xs : List Packet
⊢ levels xs + levels ys < levels xs + 2 + (levels ys + 2)
ys xs : List Packet
⊢ levels xs + levels ys < levels xs + levels ys + (2 + 2)