proposition: Fact nary_mxsum_proof : mxsum_spec (\sum_(j <- r | P j) unwrap (S_ j)) (\sum_(j <- r | P j) unwrap (mxsum_rank (S_ j))).
proof: Proof. elim/big_rec2: _ => [|j]; first by rewrite -(mxrank0 n n); left. by case: (S_ j); right. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)