Commit 2023-04-10 15:18 12d0c10f

View on Github →

feat: port Data.Num.Lemmas (#2784)

Estimated changes

added def Int.ofSnum
added theorem Num.add_ofNat'
added theorem Num.add_of_nat
added theorem Num.add_one
added theorem Num.add_succ
added theorem Num.add_toZNum
added theorem Num.add_to_nat
added theorem Num.add_zero
added theorem Num.bit0_of_bit0
added theorem Num.bit1_of_bit1
added theorem Num.bit1_succ
added theorem Num.bit_to_nat
added theorem Num.bitwise'_to_nat
added theorem Num.cast_add
added theorem Num.cast_bit0
added theorem Num.cast_bit1
added theorem Num.cast_inj
added theorem Num.cast_le
added theorem Num.cast_lt
added theorem Num.cast_mul
added theorem Num.cast_ofZNum
added theorem Num.cast_one
added theorem Num.cast_pos
added theorem Num.cast_sub'
added theorem Num.cast_succ'
added theorem Num.cast_succ
added theorem Num.cast_toZNum
added theorem Num.cast_toZNumNeg
added theorem Num.cast_to_int
added theorem Num.cast_to_nat
added theorem Num.cast_zero'
added theorem Num.cast_zero
added theorem Num.cmp_eq
added theorem Num.cmp_swap
added theorem Num.cmp_to_nat
added theorem Num.div_to_nat
added theorem Num.dvd_to_nat
added theorem Num.gcd_to_nat
added theorem Num.gcd_to_nat_aux
added theorem Num.land'_to_nat
added theorem Num.ldiff'_to_nat
added theorem Num.le_iff_cmp
added theorem Num.le_to_nat
added theorem Num.lor'_to_nat
added theorem Num.lt_iff_cmp
added theorem Num.lt_to_nat
added theorem Num.lxor'_to_nat
added theorem Num.mem_ofZNum'
added theorem Num.mod_to_nat
added theorem Num.mul_to_nat
added theorem Num.natSize_to_nat
added theorem Num.ofInt'_toZNum
added theorem Num.ofNat'_bit
added theorem Num.ofNat'_eq
added theorem Num.ofNat'_one
added theorem Num.ofNat'_succ
added theorem Num.ofNat'_zero
added theorem Num.ofZNum'_toNat
added theorem Num.ofZNum_toNat
added theorem Num.of_nat_cast
added theorem Num.of_nat_inj
added theorem Num.of_to_nat'
added theorem Num.of_to_nat
added theorem Num.ppred_to_nat
added theorem Num.pred_succ
added theorem Num.pred_to_nat
added theorem Num.shiftl_to_nat
added theorem Num.shiftr_to_nat
added theorem Num.size_eq_natSize
added theorem Num.size_to_nat
added theorem Num.sub_to_nat
added theorem Num.succ'_to_nat
added theorem Num.succ_ofInt'
added theorem Num.succ_to_nat
added theorem Num.testBit_to_nat
added theorem Num.toZNumNeg_succ
added theorem Num.toZNum_inj
added theorem Num.toZNum_succ
added theorem Num.to_nat_inj
added theorem Num.to_nat_to_int
added theorem Num.to_of_nat
added theorem Num.zero_add
added theorem Num.zneg_toZNum
added theorem Num.zneg_toZNumNeg
added theorem PosNum.add_one
added theorem PosNum.add_succ
added theorem PosNum.add_to_nat
added theorem PosNum.bit0_of_bit0
added theorem PosNum.bit1_of_bit1
added theorem PosNum.bit_to_nat
added theorem PosNum.cast_add
added theorem PosNum.cast_bit0
added theorem PosNum.cast_bit1
added theorem PosNum.cast_inj
added theorem PosNum.cast_le
added theorem PosNum.cast_lt
added theorem PosNum.cast_mul
added theorem PosNum.cast_one'
added theorem PosNum.cast_one
added theorem PosNum.cast_pos
added theorem PosNum.cast_sub'
added theorem PosNum.cast_succ
added theorem PosNum.cast_to_int
added theorem PosNum.cast_to_nat
added theorem PosNum.cast_to_num
added theorem PosNum.cast_to_znum
added theorem PosNum.cmp_eq
added theorem PosNum.cmp_swap
added theorem PosNum.cmp_to_nat
added theorem PosNum.div'_to_nat
added theorem PosNum.divMod_to_nat
added theorem PosNum.dvd_to_nat
added theorem PosNum.le_iff_cmp
added theorem PosNum.le_to_nat
added theorem PosNum.lt_iff_cmp
added theorem PosNum.lt_to_nat
added theorem PosNum.mod'_to_nat
added theorem PosNum.mul_to_nat
added theorem PosNum.natSize_pos
added theorem PosNum.natSize_to_nat
added theorem PosNum.of_to_nat'
added theorem PosNum.of_to_nat
added theorem PosNum.one_add
added theorem PosNum.one_le_cast
added theorem PosNum.one_sub'
added theorem PosNum.pred'_succ'
added theorem PosNum.pred'_to_nat
added theorem PosNum.pred_to_nat
added theorem PosNum.size_eq_natSize
added theorem PosNum.size_to_nat
added theorem PosNum.sub'_one
added theorem PosNum.succ'_pred'
added theorem PosNum.succ_to_nat
added theorem PosNum.to_nat_inj
added theorem PosNum.to_nat_pos
added theorem PosNum.to_nat_to_int
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_int_cast
added theorem ZNum.of_nat_cast
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