[Merged by Bors] - refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction#19668

YaelDillies wants to merge 2 commits intomasterleanprover-community/mathlib4:masterfrom

with_bot_inductive_leleanprover-community/mathlib4:with_bot_inductive_leCopy head branch name to clipboard