mathlib

327e83bb - finish proof of stronger version