mathlib

e52d2e47 - Redid definition of `of_bits` when trailing ff's