Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-10 03:03 fedee983

View on Github →

feat(data/nat/basic): a few choiceless proofs not sure I can take this much farther without modifying core...

Estimated changes

added theorem decidable.le_of_not_lt
added theorem decidable.le_or_lt
added theorem decidable.lt_or_le
added theorem decidable.not_lt
added theorem le_imp_le_of_lt_imp_lt
added theorem lt_iff_lt_of_le_iff_le
added theorem lt_iff_not_ge'
added theorem lt_imp_lt_of_le_imp_le
added theorem lt_of_le_of_ne'
added theorem lt_of_not_ge'
modified theorem not_le
added theorem nat.div_lt_iff_lt_mul'
added theorem nat.div_mul_le_self'
added theorem nat.le_div_iff_mul_le'