proposition: Lemma vecsum_dni {n : nat} (f : ⟦ S n ⟧%stn -> R) (j : ⟦ S n ⟧%stn ) : Σ f = op1 (Σ (f ∘ dni j)) (f j).
proof: 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.
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