mathlib

332db6a7 - add lemma suggested by Markus