proposition: Lemma wl n m (I : 'cV_n) (J : 'cV_m) : cap_wl I J *m I = cap I J.
proof: Proof. by apply: dividK; case: cap_spec. 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