Lemma vecsum_interchange : ∏ (m n : nat) (f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn -> R), Σ (λ i: (⟦ m ⟧)%stn, Σ (λ j : (⟦ n ⟧)%stn, f j i) ) = Σ (λ j: (⟦ n ⟧)%stn, Σ (λ i : (⟦ m ⟧)%stn, f j i)). Proof. intros. induction n as [| n IH]. - induction m. { reflexivity. } change (Σ (λ i : (⟦ 0 ⟧)%stn, Σ ((λ j : (⟦ _ ⟧)%stn, f i j) ))) with (@rigunel1 R). apply vecsum_zero. - rewrite vecsum_step. unfold funcomp. rewrite <- IH, <- vecsum_add. apply maponpaths, funextfun; intros i. rewrite vecsum_step. reflexivity. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Nat. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.GaussianElimination.Auxiliary.