proposition: Lemma surgery m n (M : 'M[R]_(1 + (1 + m),n)) : M = col_mx (col_mx (row 0 M) (row 1 M)) (dsubmx (dsubmx M)).
proof: Proof. apply/matrixP=> i j; rewrite !mxE; case: splitP=> k hk; rewrite !mxE. by case: splitP=> l hl; rewrite !mxE; congr fun_of_matrix; apply/ord_inj; rewrite hk hl ord1. by congr fun_of_matrix; apply/ord_inj. 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