Ico_succ_left_eq_erase_Ico

Stream: Is there code for X?

[Bolton Bailey]

Is there something like Ico_succ_left_eq_erase_Ico (a b : ℕ) : Ico a.succ b = erase (Ico a b) a?
@Yaël Dillies , I see you have recently been PRs about intervals. Do you have a plan to include something like this?

[Yakov Pechersky]

Isn't the proof just { ext, simp }?

[Bolton Bailey]

That leaves the goal a.succ ≤ a_1 ∧ a_1 < b ↔ ¬a_1 = a ∧ a ≤ a_1 ∧ a_1 < b

[Kevin Buzzard]

Can library_search solve a+1 ≤ t ↔ a ≠ t ∧ a ≤ t? Or prove that either of them are equivalent to a<t? That seems to be the missing piece.

[Yaël Dillies]

There might not be! I could have spent tens of PRs completing the finite intervals API but I decided I would wait to see what's needed. If you need it, we can add it.

[Yaël Dillies]

You should first prove Ico a.succ b = Ioo a b.

[Yakov Pechersky]

The proof for that iff should use the underlying lt lemma present in preorder, likely after an and_comm