proposition: Lemma rank_skew : \rank skew = (n * n.-1)./2.
proof: Proof. rewrite /skew (mxdirectP _) //= -bin2 -triangular_sum big_mkord. rewrite (eq_bigr (fun _ => 1%N)); last first. move=> [i j] /= lt_ij; rewrite genmxE. apply/eqP; rewrite eqn_leq rank_leq_row /= lt0n mxrank_eq0. rewrite /skew_vec /= !mxvec_delta /= subr_eq0. set j1 := mxvec_index _ _. apply/negP => /eqP /matrixP /(_ 0 j1) /=; rewrite !mxE /= eqxx. have /(_ _ _ (_, _) (_, _)) -> := inj_eq (bij_inj (onT_bij (curry_mxvec_bij _ _))). rewrite xpair_eqE -!val_eqE /= eq_sym andbb ltn_eqF //. by move/eqP; rewrite oner_eq0. transitivity (\sum_(i < n) (\sum_(j < n | j < i) 1))%N. by rewrite pair_big_dep. apply: eq_bigr => [] [[|i] Hi] _ /=; first by rewrite big1. rewrite (eq_bigl _ _ (fun _ => ltnS _ _)). have [n_eq0|n_gt0] := posnP n; first by move: Hi (Hi); rewrite {1}n_eq0. rewrite -[n]prednK // big_ord_narrow_leq /=. by rewrite -ltnS prednK // (leq_trans _ Hi). by rewrite sum_nat_const card_ord muln1. 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)