case nil
R : Type u_1
S : Type ?u.11
inst✝ : AddMonoid R
⊢ trop (sum []) = prod (map trop [])

case cons
R : Type u_1
S : Type ?u.11
inst✝ : AddMonoid R
hd : R
tl : List R
IH : trop (sum tl) = prod (map trop tl)
⊢ trop (sum (hd :: tl)) = prod (map trop (hd :: tl))
R : Type u_1
S : Type ?u.11
inst✝ : AddMonoid R
l : List R
⊢ trop (sum l) = prod (map trop l)
induction' l with hd tl IH
no goals
case nil
R : Type u_1
S : Type ?u.11
inst✝ : AddMonoid R
⊢ trop (sum []) = prod (map trop [])
simp
no goals
case cons
R : Type u_1
S : Type ?u.11
inst✝ : AddMonoid R
hd : R
tl : List R
IH : trop (sum tl) = prod (map trop tl)
⊢ trop (sum (hd :: tl)) = prod (map trop (hd :: tl))
simp [← IH]