Commit 2022-12-10 13:28 0b6f3c27

View on Github →

feat: port Data.Nat.Order.Basic (#907) 655994e298904d7e5bbd1e18c95defd7b543eb94

depends on: #905

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Nat/Basic.lean

Created Mathlib/Data/Nat/Order/Basic.lean

added theorem Nat.add_eq_max_iff

added theorem Nat.add_eq_min_iff

added theorem Nat.add_eq_one_iff

added theorem Nat.add_eq_three_iff

added theorem Nat.add_eq_two_iff

added theorem Nat.add_mod_eq_ite

added theorem Nat.add_pos_iff_pos_or_pos

added theorem Nat.add_pos_left

added theorem Nat.add_pos_right

added theorem Nat.add_succ_lt_add

added theorem Nat.diag_induction

added theorem Nat.div_dvd_of_dvd

added theorem Nat.div_eq_self

added theorem Nat.div_eq_sub_mod_div

added theorem Nat.div_mul_div_comm

added theorem Nat.div_mul_div_le_div

added theorem Nat.dvd_sub_mod

added theorem Nat.eq_one_of_mul_eq_one_left

added theorem Nat.eq_one_of_mul_eq_one_right

added theorem Nat.eq_zero_of_double_le

added theorem Nat.eq_zero_of_le_div

added theorem Nat.eq_zero_of_le_half

added theorem Nat.eq_zero_of_mul_le

added theorem Nat.findGreatest_eq_iff

added theorem Nat.findGreatest_eq_zero_iff

added theorem Nat.findGreatest_is_greatest

added theorem Nat.findGreatest_le

added theorem Nat.findGreatest_mono

added theorem Nat.findGreatest_mono_left

added theorem Nat.findGreatest_mono_right

added theorem Nat.findGreatest_of_ne_zero

added theorem Nat.findGreatest_spec

added theorem Nat.find_add

added theorem Nat.find_pos

added theorem Nat.le_add_one_iff

added theorem Nat.le_add_pred_of_pos

added theorem Nat.le_and_le_add_one_iff

added theorem Nat.le_findGreatest

added theorem Nat.le_mul_of_pos_left

added theorem Nat.le_mul_of_pos_right

added theorem Nat.le_mul_self

added theorem Nat.le_or_le_of_add_eq_add_pred

added theorem Nat.lt_mul_self_iff

added theorem Nat.lt_of_lt_pred

added theorem Nat.lt_one_iff

added theorem Nat.lt_pred_iff

added theorem Nat.max_eq_zero_iff

added theorem Nat.min_eq_zero_iff

added theorem Nat.mod_mul_left_div_self

added theorem Nat.mod_mul_right_div_self

added theorem Nat.mul_div_mul_comm_of_dvd_dvd

added theorem Nat.mul_eq_one_iff

added theorem Nat.mul_self_inj

added theorem Nat.mul_self_le_mul_self

added theorem Nat.mul_self_le_mul_self_iff

added theorem Nat.mul_self_lt_mul_self

added theorem Nat.mul_self_lt_mul_self_iff

added theorem Nat.not_dvd_of_between_consec_multiples

added theorem Nat.not_dvd_of_pos_of_lt

added theorem Nat.one_le_iff_ne_zero

added theorem Nat.one_le_of_lt

added theorem Nat.one_lt_iff_ne_zero_and_ne_one

added theorem Nat.one_mod

added theorem Nat.pred_le_iff

added theorem Nat.set_induction

added theorem Nat.set_induction_bounded

added theorem Nat.sub_mod_eq_zero_of_mod_eq

added theorem Nat.sub_succ'

added theorem Nat.succ_mul_pos

added theorem Nat.two_le_iff

added theorem Nat.two_mul_odd_div_two

added theorem Nat.zero_max

Modified Mathlib/Init/Data/Nat/Lemmas.lean

added theorem Nat.eq_zero_of_mul_eq_zero