proposition: Lemma sub_capmx_gen m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) : (A <= capmx_gen B C)%MS = (A <= B)%MS && (A <= C)%MS.
proof: Proof. apply/idP/andP=> [sAI | [/submxP[B' ->{A}] /submxP[C' eqBC']]]. rewrite !(submx_trans sAI) ?submxMl // /capmx_gen. have:= mulmx_ker (col_mx B C); set K := kermx _. rewrite -{1}[K]hsubmxK mul_row_col; move/(canRL (addrK _))->. by rewrite add0r -mulNmx submxMl. have: (row_mx B' (- C') <= kermx (col_mx B C))%MS. by rewrite sub_kermx mul_row_col eqBC' mulNmx subrr. case/submxP=> D; rewrite -[kermx _]hsubmxK mul_mx_row. by case/eq_row_mx=> -> _; rewrite -mulmxA 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)