proposition: Lemma skew_direct_sum : mxdirect skew.
proof: Proof. apply/mxdirect_sumsE => /=; split => [i _|]; first exact: mxdirect_trivial. apply/mxdirect_sumsP => [] [i j] /= lt_ij; apply/eqP; rewrite -submx0. apply/rV_subP => v; rewrite sub_capmx => /andP []; rewrite !genmxE. move=> /submxP [w ->] /sub_sums_genmxP [/= u_]. move/matrixP => /(_ 0 (mxvec_index i j)); rewrite !mxE /= big_ord1. rewrite /skew_vec /= !mxvec_delta !mxE !eqxx /=. have /(_ _ _ (_, _) (_, _)) /= eq_mviE := inj_eq (bij_inj (onT_bij (curry_mxvec_bij _ _))). rewrite eq_mviE xpair_eqE -!val_eqE /= eq_sym andbb. rewrite ltn_eqF // subr0 mulr1 summxE big1. rewrite [w as X in X *m _]mx11_scalar => ->. by rewrite mul_scalar_mx scale0r submx0. move=> [i' j'] /= /andP[lt_j'i']. rewrite xpair_eqE /= => neq'_ij. rewrite /= !mxvec_delta !mxE big_ord1 !mxE !eqxx !eq_mviE. rewrite !xpair_eqE /= [_ == i']eq_sym [_ == j']eq_sym (negPf neq'_ij) /=. set z := (_ && _); suff /negPf -> : ~~ z by rewrite subrr mulr0. by apply: contraL lt_j'i' => /andP [/eqP <- /eqP <-]; rewrite ltnNge ltnW. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)