Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-29 07:48 6997cafb

View on Github →

feat(data/nat/basic): remove superfluous assumptions

Estimated changes

added theorem nat.lt_pred_iff
deleted theorem nat.lt_pred_of_succ_lt
added theorem nat.pred_le_iff
modified theorem nat.sub_le_left_iff_le_add
modified theorem nat.sub_le_right_iff_le_add