proposition: Lemma sum_wH_row (F : ringType) n m (H : 'M[F]_(m, n)) : (\sum_(m0 : 'I_m) wH (row m0 H) = \sum_(n0 : 'I_n) wH (col n0 H)^T)%nat.
proof: Proof. transitivity (\sum_(m0 < m) \sum_(n0 < n) (H m0 n0 != 0%R))%nat. apply eq_bigr => m0 _. rewrite wH_sum; apply eq_bigr => n0 _; by rewrite mxE. rewrite exchange_big /=. apply eq_bigr => n0 _. rewrite wH_sum; apply eq_bigr => m0 _; by rewrite 2!mxE. Qed.
imports: Reals mathcomp(all_ssreflect fingroup zmodp ssralg finalg perm matrix) mathcomp(poly mxalgebra mxpoly) mathcomp(Rstruct) ssr_ext ssralg_ext f2 num_occ natbin ssrR Reals_ext bigop_ext