Lemma switch_row_matrix_involution { n : nat } ( r1 r2 : ⟦ n ⟧%stn ) : ((switch_row_matrix r1 r2) ** (switch_row_matrix r1 r2)) = @identity_matrix _ _. Proof. intros. rewrite switch_row_as_matrix. unfold switch_row, switch_row_matrix. apply funextfun; intros i. destruct (stn_eq_or_neq i r1) as [eq | neq]; destruct (stn_eq_or_neq r1 r2) as [eq' | neq']; rewrite stn_eq_or_neq_refl; simpl. - rewrite eq'; rewrite stn_eq_or_neq_refl; simpl. apply funextfun; intros j. rewrite <- eq', eq; apply idpath. - rewrite eq; simpl. rewrite (stn_eq_or_neq_right (issymm_stnneq neq')); simpl. reflexivity. - rewrite <- eq'; rewrite stn_eq_or_neq_refl; simpl. rewrite (stn_eq_or_neq_right neq); simpl. reflexivity. - rewrite stn_eq_or_neq_refl; simpl. destruct (stn_eq_or_neq _ _) as [eq | ?]; simpl. + now rewrite eq. + reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.GaussianElimination.Auxiliary. Require Import UniMath.Algebra.GaussianElimination.Vectors. Require Import UniMath.Algebra.GaussianElimination.Matrices.