proposition: 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: 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.
imports: UniMath.Foundations.PartA UniMath.MoreFoundations.PartA UniMath.Combinatorics.FiniteSequences UniMath.Algebra.BinaryOperations UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.RigsAndRings