proposition: Lemma sub_daddsmx : (B1 :&: B2 = 0)%MS -> (A <= B1 + B2)%MS -> sub_daddsmx_spec.
proof: Proof. move=> dxB /sub_addsmxP[u defA]. exists (u.1 *m B1) (u.2 *m B2); rewrite ?submxMl // => C1 C2 sCB1 sCB2. move/(canLR (addrK _)) => defC1. suffices: (C2 - u.2 *m B2 <= B1 :&: B2)%MS. by rewrite dxB submx0 subr_eq0 -defC1 defA; move/eqP->; rewrite addrK. rewrite sub_capmx -opprB -{1}(canLR (addKr _) defA) -addrA defC1. by rewrite !(eqmx_opp, addmx_sub) ?submxMl. 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)