Commit 2021-05-10 04:19 c993c936

View on Github →

import init.data.nat.lemmas

Estimated changes

Modified Mathlib/Data/Nat/Basic.lean

modified theorem Nat.Up.WF

modified theorem Nat.Up.next

modified def Nat.Up

added theorem Nat.add_div_left

added theorem Nat.add_div_right

added theorem Nat.add_mod_left

added theorem Nat.add_mod_right

added theorem Nat.add_mul_div_left

added theorem Nat.add_mul_div_right

added theorem Nat.add_mul_mod_self_left

added theorem Nat.add_mul_mod_self_right

added theorem Nat.add_one_ne_zero

added theorem Nat.add_sub_of_le

added def Nat.discriminate

added theorem Nat.div_eq_of_lt

added theorem Nat.div_eq_sub_div

added theorem Nat.div_lt_iff_lt_mul

added theorem Nat.div_lt_self

added theorem Nat.div_mul_le_self

added def Nat.eq_of_beq_eq_true

added theorem Nat.eq_of_mul_eq_mul_left

added theorem Nat.eq_zero_of_add_eq_zero

added theorem Nat.eq_zero_of_add_eq_zero_left

added theorem Nat.eq_zero_of_add_eq_zero_right

added def Nat.eq_zero_of_le_zero

added theorem Nat.eq_zero_of_mul_eq_zero

added theorem Nat.eq_zero_or_eq_succ_pred

added theorem Nat.eq_zero_or_pos

added theorem Nat.exists_eq_succ_of_ne_zero

added def Nat.le_add_left

added def Nat.le_add_right

added theorem Nat.le_div_iff_mul_le

added theorem Nat.le_lt_antisymm

added theorem Nat.le_of_le_of_sub_le_sub_right

added def Nat.le_of_lt_succ

added def Nat.le_of_succ_le

added def Nat.le_of_succ_le_succ

added def Nat.le_step

added theorem Nat.le_sub_iff_add_le

added def Nat.le_succ

added def Nat.le_succ_of_le

added theorem Nat.le_succ_of_pred_le

added theorem Nat.lt_le_antisymm

added def Nat.lt_of_succ_le

added def Nat.lt_of_succ_lt

added def Nat.lt_or_eq_of_le_succ

added theorem Nat.lt_succ_of_lt

added def Nat.lt_succ_self

added theorem Nat.mod_add_div

added theorem Nat.mul_div_le

added theorem Nat.mul_div_left

added theorem Nat.mul_div_right

added theorem Nat.mul_mod_left

added theorem Nat.mul_mod_mul_left

added theorem Nat.mul_mod_mul_right

added theorem Nat.mul_mod_right

added theorem Nat.mul_pred_left

added theorem Nat.mul_pred_right

added theorem Nat.mul_sub_div

added def Nat.nat_zero_eq_zero

added def Nat.ne_of_beq_eq_false

added def Nat.not_lt_zero

added def Nat.not_succ_le_self

added theorem Nat.not_succ_le_zero

added theorem Nat.one_add

added theorem Nat.one_pos

added theorem Nat.one_succ_zero

added def Nat.pos_pos_of_pos

added def Nat.pow_le_pow_of_le_left

added def Nat.pow_le_pow_of_le_right

added def Nat.pow_succ

added def Nat.pow_zero

added theorem Nat.pred_inj

added def Nat.pred_le

added def Nat.pred_le_pred

added def Nat.pred_lt

added theorem Nat.pred_lt_pred

added theorem Nat.pred_succ

added theorem Nat.pred_zero

added theorem Nat.sub_add_min_cancel

added theorem Nat.sub_eq_sub_min

added theorem Nat.sub_eq_zero_of_le

added def Nat.sub_induction

added def Nat.sub_le

added def Nat.sub_lt

added theorem Nat.sub_lt_self

added theorem Nat.sub_lt_succ

added theorem Nat.sub_mul_div

added theorem Nat.sub_mul_mod

added theorem Nat.sub_one

added theorem Nat.sub_one_sub_lt

added theorem Nat.sub_self_add

added theorem Nat.succ_add_eq_succ_add

added def Nat.succ_eq_add_one

added def Nat.succ_le_of_lt

added def Nat.succ_le_succ

added theorem Nat.succ_mul_succ_eq

added theorem Nat.succ_ne_self

added def Nat.succ_ne_zero

added def Nat.succ_pos

added theorem Nat.succ_pred_eq_of_pos

added theorem Nat.succ_sub

added theorem Nat.succ_sub_one

added theorem Nat.succ_sub_sub_succ

added def Nat.two_step_induction

added def Nat.zero_eq

added def Nat.zero_le

added def Nat.zero_lt_succ

Modified Mathlib/Logic/Basic.lean

added theorem Decidable.not_and

deleted def Decidable.not_and

added def WellFounded.fix'

Modified Mathlib/Tactic/Basic.lean