mathlib3
1a92c0de - feat(order/basic): add simp attribute on le_refl, zero_le_one and zero_lt_one (#7733)

Commit

4 years ago

feat(order/basic): add simp attribute on le_refl, zero_le_one and zero_lt_one (#7733) These ones show up so often that they would have deserved a simp attribute long ago.

Author

sgouezel

Parents

fd48ac55

mathlib3 1a92c0de - feat(order/basic): add simp attribute on le_refl, zero_le_one and zero_lt_one (#7733)

mathlib3
1a92c0de - feat(order/basic): add simp attribute on le_refl, zero_le_one and zero_lt_one (#7733)