[Merged by Bors] - feat(Order/Basic): Add ltByCases API

[linesthatinterlace]

I noticed that ltByCases doesn't have any API, and it would be useful to have some when working trichotomously, especially if one wishes to define things trichotomously.

A non-dependent version is also defined.

---

[linesthatinterlace]

For what it's worth, in the context of actually using these, I've found ltByCases worthwhile. This is because it calls for things of the form x < y -> P, wheras using a match h : compare x y construct gives you the requirement to make P adding the h : compare x y = LT hypothesis, say. But sometimes you want the former, because you then want to define things by cases and thus generalizing h: I am not really sure how to do that in term mode! If someone knows, please let me know... but in general I do think this adds utility.

[jcommelin]

I think this looks good now. After you add the suggested lemma, please feel free to merge this.

bors d+

[mathlib-bors]

✌️ linesthatinterlace can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style