Lemma vecsum_dni {n : nat} (f : ⟦ S n ⟧%stn -> R) (j : ⟦ S n ⟧%stn ) : Σ f = op1 (Σ (f ∘ dni j)) (f j). Proof. intros. induction j as [j J]. assert (e2 : j + (n - j) = n). { rewrite natpluscomm. apply minusplusnmm. apply natlthsntoleh. exact J. } assert (e : (S j) + (n - j) = S n). { change (S j + (n - j)) with (S (j + (n - j))). apply maponpaths. exact e2. } intermediate_path (Σ (λ i, f (transportf stn e i))). - apply (transport_vecsum e). - rewrite (vecsum_left_right (S j) (n - j)); unfold funcomp. apply pathsinv0. rewrite (transport_vecsum e2). rewrite (vecsum_left_right j (n-j)); unfold funcomp. rewrite (vecsum_step (λ x, f (transportf stn e _))); unfold funcomp. apply pathsinv0. rewrite rigassoc1. rewrite (@rigcomm1 R (f _) ). rewrite <- rigassoc1. apply map_on_two_paths. + apply map_on_two_paths. * apply vecsum_eq; intro i. induction i as [i I]. apply maponpaths. apply subtypePath_prop. induction e. rewrite idpath_transportf. rewrite stn_left_compute. unfold dni,di, stntonat; simpl. induction (natlthorgeh i j) as [R'|R']. -- unfold stntonat; simpl; rewrite transport_stn; simpl. induction (natlthorgeh i j) as [a|b]. ++ apply idpath. ++ contradicts R' (natlehneggth b). -- unfold stntonat; simpl; rewrite transport_stn; simpl. induction (natlthorgeh i j) as [V|V]. ++ contradicts I (natlehneggth R'). ++ apply idpath. * apply vecsum_eq; intro i. induction i as [i I]. apply maponpaths. unfold dni,di, stn_right, stntonat; repeat rewrite transport_stn; simpl. induction (natlthorgeh (j+i) j) as [X|X]. -- contradicts (negnatlthplusnmn j i) X. -- apply subtypePath_prop. simpl. apply idpath. + apply maponpaths. rewrite transport_stn; simpl. apply subtypePath_prop, idpath. 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.