mathlib3

b3fa928e - Merge branch 'image2-lemmas' into set-vsub