mathlib

11b42452 - add lemmas about canceling multiplication