Commit 2022-11-14 10:32 45f4c474

View on Github →

feat: port data.int.basic (#584)

  • depends on #583 The final section /-! # units -/ has not been ported, because it still depends on some earlier files.

Estimated changes

added theorem Int.coe_nat_div
added theorem Int.coe_nat_ediv
added theorem Int.coe_nat_inj'
added theorem Int.coe_nat_mod
added theorem Int.coe_nat_nonneg
added theorem Int.coe_nat_strictMono
added theorem Int.coe_pred_of_pos
added theorem Int.ediv_of_neg_of_pos
added theorem Int.neg_nat_succ
added theorem Int.neg_pred
added theorem Int.neg_succ
added def Int.pred
added theorem Int.pred_nat_succ
added theorem Int.pred_neg_pred
added theorem Int.pred_succ
added def Int.succ
added theorem Int.succ_neg_nat_succ
added theorem Int.succ_neg_succ
added theorem Int.succ_pred
added theorem Int.toNat_coe_nat
modified theorem le_refl