proposition: Lemma subid_addAl m n p (I: 'cV[R]_m) (J: 'cV[R]_n) (K: 'cV[R]_p) : (I +i (J +i K) <= (I +i J) +i K)%IS.
proof: Proof. apply/subidP. exists (block_mx (row_mx 1%:M 0) 0 (block_mx 0 1%:M 0 0) (col_mx 0 1%:M)). rewrite !mul_block_col mul_row_col mul_col_mx add_col_mx. by rewrite !(mul0mx,mul1mx,add0r,addr0). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice fingroup) mathcomp(matrix bigop zmodp mxalgebra poly) ssrcomplements