proposition: Lemma skewP (M : 'rV_(n * n)) : reflect ((vec_mx M)^T = - vec_mx M) (M <= skew)%MS.
proof: Proof. apply: (iffP idP). move/sub_sumsmxP => [v ->]; rewrite !linear_sum /=. apply: eq_bigr => [] [i j] /= lt_ij; rewrite !mulmx_sum_row !linear_sum /=. apply: eq_bigr => k _; rewrite !linearZ /=; congr (_ *: _) => {v}. set r := << _ >>%MS; move: (row _ _) (row_sub k r) => v. move: @r; rewrite /= genmxE => /sub_rVP [a ->]; rewrite !linearZ /=. by rewrite /skew_vec !linearB /= !mxvecK !scalerN opprK addrC !trmx_delta. move=> skewM; pose M' := vec_mx M. pose xM i j := (M' i j - M' j i) *: skew_vec i j. suff -> : M = 2%:R^-1 *: (\sum_(i | true && ((i.2 : 'I__) < (i.1 : 'I__))%N) xM i.1 i.2). rewrite scalemx_sub // summx_sub_sums // => [] [i j] /= lt_ij. by rewrite scalemx_sub // genmxE. rewrite /xM /= /skew_vec (eq_bigr _ (fun _ _ => scalerBr _ _ _)). rewrite big_split /= sumrN !(eq_bigr _ (fun _ _ => scalerBl _ _ _)). rewrite !big_split /= !sumrN opprD ?opprK addrACA [- _ + _]addrC. rewrite -!sumrN -2!big_split /=. rewrite /xM /= /skew_vec -!(eq_bigr _ (fun _ _ => scalerBr _ _ _)). apply: (can_inj vec_mxK); rewrite !(linearZ, linearB, linearD, linear_sum) /=. have -> /= : vec_mx M = 2%:R^-1 *: (M' - M'^T). by rewrite skewM opprK -mulr2n -scaler_nat scalerA mulVf ?pnatr_eq0 ?scale1r. rewrite [M' in LHS]matrix_sum_delta; congr (_ *: _). rewrite pair_big /= !linear_sum /= -big_split /=. rewrite (bigID (fun ij => (ij.2 : 'I__) < (ij.1 : 'I__))%N) /=; congr (_ + _). apply: eq_bigr => [] [i j] /= lt_ij. by rewrite !linearZ linearB /= ?mxvecK trmx_delta scalerN scalerBr. rewrite (bigID (fun ij => (ij.1 : 'I__) == (ij.2 : 'I__))%N) /=. rewrite big1 ?add0r; last first. by move=> [i j] /= /andP[_ /eqP ->]; rewrite linearZ /= trmx_delta subrr. rewrite (@reindex_inj _ _ _ _ (fun ij => (ij.2, ij.1))) /=; last first. by move=> [? ?] [? ?] [] -> ->. apply: eq_big => [] [i j] /=; first by rewrite -leqNgt ltn_neqAle andbC. by rewrite !linearZ linearB /= ?mxvecK trmx_delta scalerN scalerBr. 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)