mathlib3

f8121b1e - Shortened proof of encodek_num