proposition: Lemma wH_row_mx n (F : ringType) r (rn : (r <= n)%N) : wH (row_mx (const_mx 1) 0 : 'rV[F]_(r + (n - r))) = r.
proof: Proof. rewrite wH_sum (bigID (fun x : 'I__ => (x < r)%N)) /=. rewrite (eq_bigr (fun=> 1%N)); last first. move=> i ir. rewrite (_ : i = lshift _ (Ordinal ir)) ?row_mxEl ?mxE ?oner_neq0 //. by apply val_inj. rewrite sum1dep_card (eq_bigr (fun=> O)) //; last first. move=> i ir. have ir' : (i - r < n - r)%N. destruct r as [|r]. rewrite subn0. move/leq_trans: (ltn_ord i); apply; by rewrite subn0 add0n. rewrite subnS prednK // ?subn_gt0 // ?ltnNge; last by rewrite ltnS in ir. rewrite /= [in X in (_ <= X)%N]subnS. destruct n as [|n'] => //. rewrite subSKn leq_sub2r //. move: (ltn_ord i); by rewrite [in X in (_ < X)%N -> _]subnKC ltnS. rewrite (_ : i = rshift _ (Ordinal ir')); last first. apply val_inj => /=; by rewrite [in RHS]subnKC // leqNgt. by rewrite row_mxEr mxE eqxx. rewrite big_const iter_addn_0 mul0n addn0 -sum1dep_card. by rewrite big_ord_narrow ?subnKC // sum1_card card_ord. 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