Theorem Order.Ioi_pred_eq_insert_of_not_isMin

Modification history