mathlib

39e1ad2d - Merge branch 'nontriviality' into ordered_semiring_zero_le_one