proposition: Fact binary_mxsum_proof : mxsum_spec (unwrap S1 + unwrap S2) (unwrap (mxsum_rank S1) + unwrap (mxsum_rank S2)).
proof: Proof. by case: S1 S2 => [A1 r1 A1P] [A2 r2 A2P]; 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)