proposition: Lemma surgery2 m n (M : 'M[R]_(m,1 + (1 + n))) : M = row_mx (row_mx (col 0 M) (col 1 M)) (rsubmx (rsubmx M)).
proof: Proof. apply: trmx_inj; rewrite (tr_row_mx (row_mx (col 0 M) (col 1 M))). by rewrite tr_row_mx !tr_col !trmx_rsub {1}[M^T]surgery. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype matrix mxalgebra bigop zmodp perm choice) dvdring mxstructure minor stronglydiscrete coherent edr