mathlib

5064afa1 - A bad start at trying to make norm_fin work on subtraction