proposition: Lemma mxrow_recl n (B_ : forall j, 'M[T]_(n, p_ j)) : \mxrow_j B_ j = castmx (erefl, mxsize_recl) (row_mx (B_ 0) (\mxrow_j B_ (lift ord0 j))).
proof: Proof. apply/mxrowP => i; rewrite mxrowK. apply/matrixP => j k; rewrite !(castmxE, mxE)/=. case: splitP => l /=; do [ rewrite [LHS]RankEsum big_mkcond big_ord_recl -big_mkcond/=; rewrite /bump/= -addnA cast_ord_id; under eq_bigl do rewrite add1n -ltn_predRL/=]. case: posnP => i0; last first. by move=> lE; have := ltn_ord l; rewrite /= -lE -ltn_subRL subnn. by rewrite (@val_inj _ _ _ i 0 i0) big_pred0_eq in k * => /val_inj->. case: posnP => i0. rewrite (@val_inj _ _ _ i 0 i0) big_pred0_eq in k l * => kE. by have := ltn_ord k; rewrite /= [val k]kE -ltn_subRL subnn. have i_lt : i.-1 < m by rewrite -subn1 ltn_subLR. set i' := lift ord0 (Ordinal i_lt). have ii' : i = i' by apply/val_inj; rewrite /=/bump/= add1n prednK. have k_lt : k < p_ i' by rewrite -ii'. move=> /addnI; rewrite eqRank => /val_inj/= /[dup] kl<-; rewrite mxE. rewrite Rank2K//; case: _ / esym; rewrite cast_ord_id/=. rewrite -/i'; set j' := Ordinal _; have : k = j' :> nat by []. by move: j'; rewrite -ii' => j' /val_inj->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)