Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Matrix inequalities for comparison

Block-matrix expressions used in the doubling-of-variables proof of comparison. The development lives in the MatrixInequalities/ submodules; this file re-exports all of them.