Commit 2024-09-08 12:47 3e01fe25

View on Github →

chore(Order/SuccPred/Basic): Move succ/pred being archimedean to a different file (#16559) Also prove le_total_of_ge, le_total_of_le, lt_or_le_of_ge, lt_or_le_of_le.

Estimated changes

added theorem Pred.rec
added theorem Pred.rec_iff
added theorem Pred.rec_linear
added theorem Pred.rec_top
added theorem Succ.rec
added theorem Succ.rec_bot
added theorem Succ.rec_iff
added theorem Succ.rec_linear
added theorem exists_pred_iterate_or
added theorem exists_succ_iterate_or
added theorem pred_max
added theorem pred_min
added theorem succ_max
added theorem succ_min
deleted theorem LE.le.exists_pred_iterate
deleted theorem LE.le.exists_succ_iterate
deleted theorem Pred.rec
deleted theorem Pred.rec_iff
deleted theorem Pred.rec_linear
deleted theorem Pred.rec_top
deleted theorem Succ.rec
deleted theorem Succ.rec_bot
deleted theorem Succ.rec_iff
deleted theorem Succ.rec_linear
deleted theorem exists_pred_iterate_or
deleted theorem exists_succ_iterate_or
deleted theorem pred_max
deleted theorem pred_min
deleted theorem succ_max
deleted theorem succ_min