proposition: 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: 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.
imports: UniMath.Foundations.PartA UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.Matrix UniMath.Algebra.GaussianElimination.Auxiliary