Commit 2024-01-10 08:02 497ed074

View on Github →

refactor: Split off basic Nat file (#9551) Data.Nat.Basic is currently made of two things:

  • Basic lemmas that continue the theory in Std (and could belong there, really)
  • Basic algebraic order instances I need the first ones earlier in the algebraic order hierarchy, hence the split. Part of #9411. Similar to #9443

Estimated changes

deleted theorem LT.lt.nat_succ_le
deleted theorem Nat.add_def
deleted theorem Nat.add_one_le_iff
deleted theorem Nat.add_succ_sub_one
deleted theorem Nat.and_forall_succ
deleted theorem Nat.div_add_mod'
deleted theorem Nat.div_le_div_left
deleted theorem Nat.div_lt_iff_lt_mul'
deleted theorem Nat.div_lt_one_iff
deleted theorem Nat.div_lt_self'
deleted theorem Nat.div_mul_div_comm
deleted theorem Nat.eq_of_le_of_lt_succ
deleted theorem Nat.exists_eq_add_of_le'
deleted theorem Nat.exists_eq_add_of_le
deleted theorem Nat.exists_eq_add_of_lt
deleted theorem Nat.exists_lt_succ
deleted theorem Nat.findGreatest_eq
deleted theorem Nat.findGreatest_of_not
deleted theorem Nat.findGreatest_succ
deleted theorem Nat.findGreatest_zero
deleted theorem Nat.find_comp_succ
deleted theorem Nat.find_eq_iff
deleted theorem Nat.find_eq_zero
deleted theorem Nat.find_le
deleted theorem Nat.find_le_iff
deleted theorem Nat.find_lt_iff
deleted theorem Nat.find_mono
deleted theorem Nat.forall_lt_succ
deleted def Nat.leRecOn'
deleted def Nat.leRecOn
deleted theorem Nat.leRecOn_injective
deleted theorem Nat.leRecOn_self
deleted theorem Nat.leRecOn_succ'
deleted theorem Nat.leRecOn_succ
deleted theorem Nat.leRecOn_succ_left
deleted theorem Nat.leRecOn_surjective
deleted theorem Nat.leRecOn_trans
deleted theorem Nat.le_div_iff_mul_le'
deleted theorem Nat.le_find_iff
deleted theorem Nat.le_induction
deleted theorem Nat.le_of_pred_lt
deleted theorem Nat.lt_add_one_iff
deleted theorem Nat.lt_div_mul_add
deleted theorem Nat.lt_find_iff
deleted theorem Nat.lt_iff_add_one_le
deleted theorem Nat.lt_iff_le_pred
deleted theorem Nat.lt_mul_div_succ
deleted theorem Nat.lt_mul_of_div_lt
deleted theorem Nat.lt_of_div_lt_div
deleted theorem Nat.lt_one_add_iff
deleted theorem Nat.lt_succ_iff
deleted theorem Nat.lt_succ_iff_lt_or_eq
deleted theorem Nat.mod_add_div'
deleted theorem Nat.mod_eq_iff_lt
deleted theorem Nat.mod_mod_of_dvd
deleted theorem Nat.mod_succ
deleted theorem Nat.mod_succ_eq_iff_lt
deleted theorem Nat.mul_add_mod'
deleted theorem Nat.mul_add_mod_of_lt
deleted theorem Nat.mul_def
deleted theorem Nat.mul_dvd_of_dvd_div
deleted theorem Nat.mul_left_eq_self_iff
deleted theorem Nat.mul_ne_mul_left
deleted theorem Nat.mul_ne_mul_right
deleted theorem Nat.mul_right_eq_self_iff
deleted theorem Nat.not_succ_lt_self
deleted theorem Nat.of_le_succ
deleted theorem Nat.one_add_le_iff
deleted theorem Nat.one_le_div_iff
deleted theorem Nat.one_lt_mul_iff
deleted theorem Nat.one_lt_succ_succ
deleted theorem Nat.or_exists_succ
deleted def Nat.pincerRecursion
deleted theorem Nat.pred_add_self
deleted theorem Nat.pred_eq_of_eq_succ
deleted theorem Nat.pred_eq_self_iff
deleted theorem Nat.pred_eq_sub_one
deleted theorem Nat.pred_eq_succ_iff
deleted theorem Nat.pred_one_add
deleted theorem Nat.pred_sub
deleted theorem Nat.rec_add_one
deleted theorem Nat.rec_zero
deleted theorem Nat.self_add_pred
deleted theorem Nat.self_add_sub_one
deleted def Nat.strongRecOn'
deleted theorem Nat.strongRecOn'_beta
deleted theorem Nat.sub_one_add_self
deleted theorem Nat.succ_add_sub_one
deleted theorem Nat.succ_injective
deleted theorem Nat.succ_le_iff
deleted theorem Nat.succ_ne_succ
deleted theorem Nat.succ_pos'
deleted theorem Nat.succ_succ_ne_one
deleted theorem Nat.two_lt_of_ne
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.div_mul_div_comm
added theorem Nat.exists_lt_succ
added def Nat.findGreatest
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.le_succ_iff
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.mod_add_div'
added theorem Nat.mod_eq_iff_lt
added theorem Nat.mod_mod_of_dvd
added theorem Nat.mod_succ
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_eq_left
added theorem Nat.mul_eq_right
added theorem Nat.not_succ_lt_self
added theorem Nat.one_add_le_iff
added theorem Nat.one_le_div_iff
added theorem Nat.one_le_iff_ne_zero
added theorem Nat.one_lt_mul_iff
added theorem Nat.one_lt_succ_succ
added theorem Nat.or_exists_succ
added theorem Nat.pred_add_self
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 theorem Nat.self_add_pred
added theorem Nat.self_add_sub_one
added def Nat.strongRecOn'
added theorem Nat.strongRecOn'_beta
added theorem Nat.sub_one_add_self
added theorem Nat.succ_add_sub_one
added theorem Nat.succ_injective
added theorem Nat.succ_le_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 theorem Nat.one_le_iff_ne_zero