proposition: Lemma switch_row_matrix_involution { n : nat } ( r1 r2 : ⟦ n ⟧%stn ) : ((switch_row_matrix r1 r2) ** (switch_row_matrix r1 r2)) = @identity_matrix _ _.
proof: 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.
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