proposition: Lemma mxdirect_addsE (S1 : mxsum_expr m1 n) (S2 : mxsum_expr m2 n) : mxdirect (unwrap S1 + unwrap S2) = [&& mxdirect (unwrap S1), mxdirect (unwrap S2) & unwrap S1 :&: unwrap S2 == 0]%MS.
proof: Proof. rewrite (@mxdirectE n) /=. have:= leqif_add (mxrank_sum_leqif S1) (mxrank_sum_leqif S2). move/(leqif_trans (mxrank_adds_leqif (unwrap S1) (unwrap S2)))=> ->. by rewrite andbC -andbA submx0. 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)