proposition: Lemma bcap_wrP n m (I : 'cV_n) (J : 'cV_m) : bcap_wr I J *m J = 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 b := principal_gen _; set a := principal_gen _. have [-> | a0] := eqVneq a 0; first by rewrite lcmr0 mulr0. have [-> | b0] := eqVneq b 0. by rewrite lcm0r odiv0r /= ?mul0r // gcdr_eq0 negb_and eqxx. case: odivrP => /= => [x Hx | H]. apply/(@mulIf _ (gcdr b a)); first by rewrite gcdr_eq0 negb_and b0. by rewrite -mulrA mulrCA -Hx mulr_lcm_gcd mulrC. case/dvdrP: (dvdr_gcdl 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