proposition: Lemma dimv_leq_sum I r (P : pred I) (Us : I -> {vspace vT}) : \dim (\sum_(i <- r | P i) Us i) <= \sum_(i <- r | P i) \dim (Us i).
proof: Proof. elim/big_rec2: _ => [|i d vs _ le_vs_d]; first by rewrite dim_vline eqxx. by apply: (leq_trans (dimv_add_leqif _ _)); rewrite leq_add2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)