order on bool

Stream: general

[Rob Lewis]

See the discussion here: https://github.com/leanprover-community/mathlib/pull/2637#discussion_r440039075
Mario questions putting a global order instance on bool. It doesn't matter much to me -- I only need it locally -- but I don't really see the harm in the global instance. Am I missing something?

(There's a stronger lattice structure on bool too, of course, but I'm not interested in setting it up for this PR.)

[Floris van Doorn]

I don't see the harm either.

[Bryan Gin-ge Chen]

@Mario Carneiro is this the only thing holding up this PR?