Commit 2023-01-16 11:59 4bb68715

View on Github →

feat: port Data.Int.SuccPred (#1543)

Estimated changes

added theorem Int.covby_add_one
added theorem Int.pos_iff_one_le
added theorem Int.pred_eq_pred
added theorem Int.pred_iterate
added theorem Int.sub_one_covby
added theorem Int.succ_eq_succ
added theorem Int.succ_iterate
added theorem Nat.cast_int_covby_iff