feat: add Bool.dand and Ordering.dthen along with more lemmas

[Rob23oba]

This PR adds Bool.dand, the dependent version of Bool.and, and Ordering.dthen, the dependent version of Ordering.then, along with new lemmas both for the non-dependent and for the dependent versions. Additionally, it adds a Decidable instance that's useful for case distinction in proofs about functions like Ordering.dthen. These primitives will be useful for implementing the new BEq / Ord / DecidableEq deriving handlers in #14929.

[TwoFX]

!radar

[leanprover-radar]

Benchmark results for 748aed9 against 2c2bdd9 are in. There are significant results. @TwoFX

• ✅ build//instructions: -1.6G (-0.01%)

Large changes (1🟥)

• 🟥 compiled/parser//instructions: +100.0M (+0.28%)

Small changes (4✅, 11🟥)

• 🟥 build/module/Init.Data.Iterators.Lemmas.Consumers//instructions: +594.5k (+0.13%)
• 🟥 build/module/Init.Data.Ord.Basic//instructions: +470.5M (+13.30%) (reduced significance based on *//lines)
• ✅ build/module/Init.Data.Slice.List//instructions: -2.0M (-0.41%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.String.Pattern//instructions: +683.6k (+0.14%)
• 🟥 build/module/Init.Internal.Order//instructions: +320.4k (+0.07%)
• 🟥 build/module/Init.Prelude//instructions: +30.2M (+0.27%)
• 🟥 build/module/Init.PropLemmas//instructions: +86.0M (+1.67%) (reduced significance based on *//lines)
• 🟥 build/module/Init.SimpLemmas//instructions: +143.1M (+6.79%) (reduced significance based on *//lines)
• ✅ build/module/Lean.ErrorExplanation//instructions: -8.9M (-0.75%)
• 🟥 build/module/Lean.Server.Snapshots//instructions: +11.8M (+1.32%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Tactic.BVDecide.Normalize//instructions: +5.8M (+1.10%) (reduced significance based on absolute threshold)
• 🟥 compiled/qsort//task-clock: +30ms (+2.72%)
• 🟥 compiled/qsort//wall-clock: +30ms (+2.75%)
• ✅ elab/lift_lets_parallel//task-clock: -31ms (-4.41%)
• ✅ elab/lift_lets_parallel//wall-clock: -31ms (-4.32%)