mathlib

f4bdf81d - add `zero_lt_one_of_pos`