Round-six lemma `isPiv_side`

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

The following holds (Lean statement, in the scope of module Solutions.R6BitNBRk):

theorem IntMul.Kappa.R6.Bit.NB.isPiv_side {m n : ℕ} (hnm : n ≤ m) (Bm : Matrix (Fin m) (Fin n) K)
    (M : Matrix (Fin n) (Fin n) K) (Am : Matrix (Fin n) (Fin m) K)
    (hB : ∀ i j : Fin n, i < j → Bm ⟨i.val, by omega⟩ j = 0)
    (hBd : ∀ i : Fin n, Bm ⟨i.val, by omega⟩ i ≠ 0)
    (hA : ∀ i j : Fin n, i < j → Am i ⟨m - n + j.val, by omega⟩ = 0)
    (hAd : ∀ i : Fin n, Am i ⟨m - n + i.val, by omega⟩ ≠ 0)
    {i j : ℕ} (h : IsPiv M i j) : IsPiv (Bm * M * Am) i (m - n + j)

Context. Round six, bit network: pivot lemmas

• isPiv_block: pivots of a block in the top-right part pass to the whole matrix.
• isPiv_diag_of_lower: a lower triangular matrix with nonzero diagonal pivots on its diagonal.
• isPiv_mid: an idempotent of rank m - k with invertible k × k corner pivots on the middle diagonal (CornerLib.solution).
• isPiv_rank1_lower: a matrix that is rank one strictly above the diagonal pivots at (l, l).
• rk_mul_lower, isPiv_side: lower triangular factors keep the rank profile; the pivots of B M A (B with lower triangular top, A with lower triangular right end) are those of M, moved to the top-right corner.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).