proposition: Lemma switch_row_matrix_invertible { n : nat } ( r1 r2 : ⟦ n ⟧%stn ) : @matrix_inverse R n (switch_row_matrix r1 r2).
proof: Proof. exists (switch_row_matrix r1 r2). split; apply switch_row_matrix_involution. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.Algebra.Matrix UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.Domains_and_Fields UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors UniMath.Algebra.GaussianElimination.Matrices