Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-06 22:11 e286452d

View on Github →

feat(data/nat/basic): some lemmas (#792)

  • feat(data/nat/basic): some lemmas
  • fixing namespace, moving lemma

Estimated changes

added theorem nat.le_pred_of_lt
added theorem nat.one_le_of_lt
added theorem nat.pred_one_add