α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
hd : α
tl : List α
a : α
⊢ length (if r a hd then a :: hd :: tl else hd :: orderedInsert r a tl) = Nat.succ (length tl) + 1
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
hd : α
tl : List α
a : α
⊢ length (orderedInsert r a (hd :: tl)) = length (hd :: tl) + 1
dsimp [orderedInsert]
no goals
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
hd : α
tl : List α
a : α
⊢ length (if r a hd then a :: hd :: tl else hd :: orderedInsert r a tl) = Nat.succ (length tl) + 1
split_ifs <;> simp [orderedInsert_length tl]