proposition: Lemma prod_minor_seq : \prod_(i < k) s`_i = minor [ffun x : 'I_k => widen_minl (widen_ord Hk x)] [ffun x : 'I_k => widen_minr (widen_ord Hk x)] (diag_mx_seq m n s).
proof: Proof. rewrite /minor /submatrix. elim: k Hk=>[H|j /= IHj Hj]; first by rewrite det_mx00 big_ord0. have IH:= ltnW Hj. apply: esym; rewrite (expand_det_row _ ord_max) big_ord_recr /= big1 ?add0r. rewrite /cofactor /col' /row' !mxE !ffunE !matrix_comp. rewrite eqxx exprD -expr2 sqrr_sign mul1r. set M := matrix_of_fun _ _. have ->: M = (\matrix_(i, j) (diag_mx_seq m n s) ([ffun x => widen_minl (widen_ord IH x)] i) ([ffun x => widen_minr (widen_ord IH x)] j)). apply/matrixP=> i l; rewrite !mxE !ffunE. have Hr: forall p, widen_ord Hj (lift ord_max p) = widen_ord IH p. by move=> p; apply: ord_inj=> /=; rewrite /bump leqNgt (ltn_ord p) add0n. by rewrite !Hr. by rewrite -(IHj IH) big_ord_recr /= mulrC. move=> i _; rewrite !mxE !ffunE /=. by rewrite eqn_leq leqNgt (ltn_ord i) andFb mul0r. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_fingroup) mathcomp(all_real_closed) CoqEAL(binetcauchy ssrcomplements mxstructure minor) CoqEAL(smith dvdring polydvd) CoqEAL(similar perm_eq_image)