refactor: port below and brecOn construction to Lean

[nomeata]

This ports the .below and .brecOn constructions to lean.

I kept them in the same file, as they were in the C code, because they are
highly coupled and the constructions are very analogous.

For validation I developed this in a separate repository at
https://github.com/nomeata/lean-constructions/tree/fad715e
and checked that all declarations found in Lean and Mathlib are
equivalent, up to

def canon (e : Expr) : CoreM Expr := do
  Core.transform (← Core.betaReduce e) (pre := fun
    | .const n ls  => return .done (.const n (ls.map (·.normalize)))
    | .sort l => return .done (.sort l.normalize)
    | _ => return .continue)

It was not feasible to make them completely equal, because the kernel's
type inference code seem to optimize level expressions a bit less
aggressively, and beta-reduces less in inference.

The private helper functions about PProd can later move into their own
file, used by these constructions as well as the structural recursion
module.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1f732bb3b7fa8e93ca01c1b257668aee14d72d2d --onto 357b52928f905bfb85a3496e411cf12fa20e730c. (2024-06-20 15:27:12)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 378b02921d930ff805b8111a1ece04abc905b963 --onto 24d51b90cc4adbc68386671bba4587d6e47188d6. (2024-06-23 08:14:28)