simp changes with_top to with_bot

Stream: general

[Gabriel Ebner]

I was somewhat to surprised that with_bot.coe_add can not only rewrite with_top, but the result then contains typeclass instances for with_bot... (This caused apply and rw to fail later on, but I'm not exactly sure why.)

import algebra.ordered_group

set_option pp.implicit true
set_option pp.notation false
example (x y : nat) : ((x + y : nat) : with_top nat) = (42 : nat) :=
begin
  simp,
  trace_state, -- look at the has_add instance
end