proposition: Lemma bcap_spec m n (I : 'cV[R]_m) (J : 'cV[R]_n) : @int_spec _ _ m n I J (bcap I J).
proof: Proof. split. - by apply/subidP; exists (bcap_wl I J); rewrite bcap_wlP. - by apply/subidP; exists (bcap_wr I J); rewrite bcap_wrP. move=> /= x. case/memberP => I' hI'. case/memberP => J' hJ'. apply/memberP. have h1 : exists I'0 : 'rV_m, I'0 *m I = x%:M by exists I'. have h2 : exists J'0 : 'rV_n, J'0 *m J = x%:M by exists J'. case: (bcap_int h1 h2) => D hD. by exists D. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice matrix bigop zmodp mxalgebra poly) ssrcomplements dvdring stronglydiscrete