Commit 2022-11-30 18:00 80eed250

View on Github →

feat: port Data.Nat.Basic (#729) This is based on a future version of mathlib3, once https://github.com/leanprover-community/mathlib/pull/17763 and https://github.com/leanprover-community/mathlib/pull/17759 have landed.

Estimated changes

added theorem Nat.Up.WF
added theorem Nat.Up.next
added def Nat.Up
added def Nat.upRel
added theorem LT.lt.nat_succ_le
deleted theorem Nat.Up.WF
deleted theorem Nat.Up.next
deleted def Nat.Up
added theorem Nat.add_def
added theorem Nat.add_one_le_iff
added theorem Nat.add_succ_sub_one
added theorem Nat.and_forall_succ
added theorem Nat.div_add_mod'
added theorem Nat.div_le_div_left
added theorem Nat.div_lt_iff_lt_mul'
added theorem Nat.div_lt_one_iff
added theorem Nat.div_lt_self'
added theorem Nat.exists_lt_succ
added theorem Nat.findGreatest_eq
added theorem Nat.findGreatest_succ
added theorem Nat.findGreatest_zero
added theorem Nat.find_comp_succ
added theorem Nat.find_eq_iff
added theorem Nat.find_eq_zero
added theorem Nat.find_le
added theorem Nat.find_le_iff
added theorem Nat.find_lt_iff
added theorem Nat.find_mono
added theorem Nat.forall_lt_succ
added def Nat.leRecOn'
added def Nat.leRecOn
added theorem Nat.leRecOn_injective
added theorem Nat.leRecOn_self
added theorem Nat.leRecOn_succ'
added theorem Nat.leRecOn_succ
added theorem Nat.leRecOn_succ_left
added theorem Nat.leRecOn_surjective
added theorem Nat.leRecOn_trans
added theorem Nat.le_div_iff_mul_le'
added theorem Nat.le_find_iff
added theorem Nat.le_induction
added theorem Nat.le_of_pred_lt
added theorem Nat.lt_add_one_iff
added theorem Nat.lt_div_mul_add
added theorem Nat.lt_find_iff
added theorem Nat.lt_iff_add_one_le
added theorem Nat.lt_iff_le_pred
added theorem Nat.lt_mul_div_succ
added theorem Nat.lt_mul_of_div_lt
added theorem Nat.lt_of_div_lt_div
added theorem Nat.lt_one_add_iff
added theorem Nat.lt_succ_iff
added theorem Nat.max_succ_succ
added theorem Nat.mod_add_div'
added theorem Nat.mod_eq_iff_lt
added theorem Nat.mod_mod_of_dvd
added theorem Nat.mod_succ_eq_iff_lt
added theorem Nat.mul_add_mod
added theorem Nat.mul_add_mod_of_lt
added theorem Nat.mul_def
added theorem Nat.mul_dvd_of_dvd_div
added theorem Nat.mul_ne_mul_left
added theorem Nat.mul_ne_mul_right
added theorem Nat.not_succ_lt_self
added theorem Nat.of_le_succ
added theorem Nat.one_add_le_iff
added theorem Nat.one_le_div_iff
added theorem Nat.one_lt_succ_succ
added theorem Nat.or_exists_succ
added theorem Nat.pred_eq_of_eq_succ
added theorem Nat.pred_eq_self_iff
added theorem Nat.pred_eq_sub_one
added theorem Nat.pred_eq_succ_iff
added theorem Nat.pred_one_add
added theorem Nat.pred_sub
added theorem Nat.rec_add_one
added theorem Nat.rec_zero
added def Nat.strongRecOn'
added theorem Nat.strongRecOn'_beta
added theorem Nat.succ_add_sub_one
added theorem Nat.succ_injective
added theorem Nat.succ_le_iff
added theorem Nat.succ_lt_succ_iff
added theorem Nat.succ_ne_succ
added theorem Nat.succ_pos'
added theorem Nat.succ_succ_ne_one
added theorem Nat.two_lt_of_ne
deleted def Nat.upRel