proposition: Lemma addsmxE : (A + B :=: col_mx A B)%MS.
proof: Proof. have:= submx_refl (col_mx A B); rewrite col_mx_sub; case/andP=> sAS sBS. rewrite unlock; do 2?case: eqP => [AB0 | _]; last exact: genmxE. by apply/eqmxP; rewrite !eqmx_sum_nop sBS col_mx_sub AB0 sub0mx /=. by apply/eqmxP; rewrite !eqmx_sum_nop sAS col_mx_sub AB0 sub0mx andbT /=. 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)