Commit 2025-04-08 11:56 ddfe6b0a

View on Github →

chore: split Data.Num.Lemmas (#23655) I have taken out a large block of statements (and a few tactics) that use ZNum or rely on statements that use ZNum and put them into Data.Num.ZNum.

Estimated changes

deleted theorem Num.cast_ofZNum
deleted theorem Num.cast_sub'
deleted theorem Num.div_to_nat
deleted theorem Num.dvd_iff_mod_eq_zero
deleted theorem Num.gcd_to_nat
deleted theorem Num.gcd_to_nat_aux
deleted theorem Num.mem_ofZNum'
deleted theorem Num.mod_to_nat
deleted theorem Num.ofInt'_toZNum
deleted theorem Num.ofZNum'_toNat
deleted theorem Num.ofZNum_toNat
deleted theorem Num.pred_succ
deleted theorem Num.sub_to_nat
deleted theorem Num.succ_ofInt'
modified theorem Num.toNat_injective
deleted theorem Num.toZNumNeg_succ
deleted theorem Num.toZNum_succ
deleted theorem PosNum.cast_sub'
deleted theorem PosNum.cast_to_znum
deleted theorem PosNum.div'_to_nat
deleted theorem PosNum.divMod_to_nat
deleted theorem PosNum.divMod_to_nat_aux
deleted theorem PosNum.mod'_to_nat
deleted theorem ZNum.abs_toZNum
deleted theorem ZNum.abs_to_nat
deleted theorem ZNum.add_one
deleted theorem ZNum.add_zero
deleted theorem ZNum.bit0_of_bit0
deleted theorem ZNum.bit1_of_bit1
deleted theorem ZNum.cast_add
deleted theorem ZNum.cast_bit0
deleted theorem ZNum.cast_bit1
deleted theorem ZNum.cast_bitm1
deleted theorem ZNum.cast_inj
deleted theorem ZNum.cast_le
deleted theorem ZNum.cast_lt
deleted theorem ZNum.cast_mul
deleted theorem ZNum.cast_neg
deleted theorem ZNum.cast_one
deleted theorem ZNum.cast_pos
deleted theorem ZNum.cast_sub
deleted theorem ZNum.cast_succ
deleted theorem ZNum.cast_to_int
deleted theorem ZNum.cast_zero'
deleted theorem ZNum.cast_zero
deleted theorem ZNum.cast_zneg
deleted theorem ZNum.cmp_to_int
deleted theorem ZNum.div_to_int
deleted theorem ZNum.dvd_iff_mod_eq_zero
deleted theorem ZNum.dvd_to_int
deleted theorem ZNum.gcd_to_nat
deleted theorem ZNum.le_to_int
deleted theorem ZNum.lt_to_int
deleted theorem ZNum.mod_to_int
deleted theorem ZNum.mul_to_int
deleted theorem ZNum.neg_of_int
deleted theorem ZNum.neg_zero
deleted theorem ZNum.ofInt'_eq
deleted theorem ZNum.ofInt'_neg
deleted theorem ZNum.of_intCast
deleted theorem ZNum.of_natCast
deleted theorem ZNum.of_nat_toZNum
deleted theorem ZNum.of_nat_toZNumNeg
deleted theorem ZNum.of_to_int'
deleted theorem ZNum.of_to_int
deleted theorem ZNum.to_int_inj
deleted theorem ZNum.to_of_int
deleted theorem ZNum.zero_add
deleted theorem ZNum.zneg_bit1
deleted theorem ZNum.zneg_bitm1
deleted theorem ZNum.zneg_neg
deleted theorem ZNum.zneg_pos
deleted theorem ZNum.zneg_pred
deleted theorem ZNum.zneg_succ
deleted theorem ZNum.zneg_zneg
added theorem Num.cast_ofZNum
added theorem Num.cast_sub'
added theorem Num.div_to_nat
added theorem Num.gcd_to_nat
added theorem Num.gcd_to_nat_aux
added theorem Num.mem_ofZNum'
added theorem Num.mod_to_nat
added theorem Num.ofInt'_toZNum
added theorem Num.ofZNum'_toNat
added theorem Num.ofZNum_toNat
added theorem Num.pred_succ
added theorem Num.sub_to_nat
added theorem Num.succ_ofInt'
added theorem Num.toZNumNeg_succ
added theorem Num.toZNum_succ
added theorem PosNum.cast_sub'
added theorem PosNum.cast_to_znum
added theorem PosNum.div'_to_nat
added theorem PosNum.divMod_to_nat
added theorem PosNum.mod'_to_nat
added theorem ZNum.abs_toZNum
added theorem ZNum.abs_to_nat
added theorem ZNum.add_one
added theorem ZNum.add_zero
added theorem ZNum.bit0_of_bit0
added theorem ZNum.bit1_of_bit1
added theorem ZNum.cast_add
added theorem ZNum.cast_bit0
added theorem ZNum.cast_bit1
added theorem ZNum.cast_bitm1
added theorem ZNum.cast_inj
added theorem ZNum.cast_le
added theorem ZNum.cast_lt
added theorem ZNum.cast_mul
added theorem ZNum.cast_neg
added theorem ZNum.cast_one
added theorem ZNum.cast_pos
added theorem ZNum.cast_sub
added theorem ZNum.cast_succ
added theorem ZNum.cast_to_int
added theorem ZNum.cast_zero'
added theorem ZNum.cast_zero
added theorem ZNum.cast_zneg
added theorem ZNum.cmp_to_int
added theorem ZNum.div_to_int
added theorem ZNum.dvd_to_int
added theorem ZNum.gcd_to_nat
added theorem ZNum.le_to_int
added theorem ZNum.lt_to_int
added theorem ZNum.mod_to_int
added theorem ZNum.mul_to_int
added theorem ZNum.neg_of_int
added theorem ZNum.neg_zero
added theorem ZNum.ofInt'_eq
added theorem ZNum.ofInt'_neg
added theorem ZNum.of_intCast
added theorem ZNum.of_natCast
added theorem ZNum.of_nat_toZNum
added theorem ZNum.of_nat_toZNumNeg
added theorem ZNum.of_to_int'
added theorem ZNum.of_to_int
added theorem ZNum.to_int_inj
added theorem ZNum.to_of_int
added theorem ZNum.zero_add
added theorem ZNum.zneg_bit1
added theorem ZNum.zneg_bitm1
added theorem ZNum.zneg_neg
added theorem ZNum.zneg_pos
added theorem ZNum.zneg_pred
added theorem ZNum.zneg_succ
added theorem ZNum.zneg_zneg