Lemma weighting_coweighting_sum {m n : nat} (mat : Matrix R m n) (wei : weighting mat) (cowei : coweighting mat) (assocax : matrix_mult_assoc_statement) : Σ (pr1 wei) = Σ (pr1 cowei). Proof. apply (invmaponpathsweq weq_matrix_1_1). intermediate_path ((row_vec (const_vec (1%rig))) ** (col_vec (pr1 wei))). - apply sum_entries1. - refine (!maponpaths (λ z, z ** _) (pr2 cowei) @ _). refine (assocax _ _ _ _ _ _ _ @ _). refine (maponpaths (λ z, _ ** z) (pr2 wei) @ _). apply pathsinv0, sum_entries2 . Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Combinatorics.FiniteSequences. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.RigsAndRings.