proposition: Lemma bcap_int (x : 'M_1) (m n : nat) (I : 'cV_m) (J : 'cV_n) : (exists I' : 'rV_m, I' *m I = x) -> (exists J' : 'rV_n, J' *m J = x) -> exists W : 'M_1, W *m bcap I J = x.
proof: Proof. case => I' HI' [J' HJ']. move: (principal_w2_correct I). move: (principal_w2_correct J). rewrite /bcap /principal. set a := principal_gen I; set b := principal_gen J => Hb Ha. have div1 : (a %| x 0 0)%R. apply/dvdrP. exists ((I' *m principal_w2 I) 0 0). move: HI'. rewrite -{1}Ha => <-. by rewrite mulrC mul_mx_scalar -scalemxAr !mxE. have div2 : (b %| x 0 0)%R. apply/dvdrP. exists ((J' *m principal_w2 J) 0 0). move: HJ'. rewrite -{1}Hb => <-. by rewrite mulrC mul_mx_scalar -scalemxAr !mxE. move/dvdrP: (dvdr_lcm a b (x 0 0)). rewrite div1 div2 /= => [[y Hy]]. exists y%:M. by rewrite -scalar_mxM -Hy -mx11_scalar. 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