mathlib

58bbbae0 - Don't need this type ascription anymore