proposition: Lemma bcap_wlP m n (I : 'cV_m) (J : 'cV_n) : bcap_wl I J *m I = bcap I J.
proof: Proof. rewrite /bcap_wl /bcap -mulmxA principal_w1_correct mul_scalar_mx. apply/rowP => i; rewrite !mxE !ord1 {i} /= !mulr1n. set a := principal_gen _; set b := principal_gen _. have [-> | b0] := eqVneq b 0; first by rewrite lcm0r mulr0. have [-> | a0] := eqVneq a 0. by rewrite lcmr0 odiv0r /= ?mul0r // gcdr_eq0 negb_and b0. case: odivrP => /= => [x Hx | H]. apply/(@mulIf _ (gcdr b a)); first by rewrite gcdr_eq0 negb_and b0. by rewrite mulr_lcm_gcd -mulrA mulrCA -Hx. case/dvdrP: (dvdr_gcdr b a) => x /eqP Hx. by move: (H x); rewrite Hx. 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