feat(data/nat/interval): add Ico_succ_left_eq_erase (#10386)
Adds `Ico_succ_left_eq_erase`. Also adds a few order lemmas needed for this.
See [this discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Ico_succ_left_eq_erase_Ico/near/259180476)
