proposition: Lemma bmember_correct : forall n (x : R) (I : 'cV[R]_n), member_spec x I (bmember x I).
proof: Proof. rewrite /bmember => n x I. case: odivrP => [a | ] Ha /=; constructor. by rewrite -mulmxA principal_w1_correct Ha scalar_mxM. move => J. rewrite -(principal_w2_correct I) /principal mulmxA scalar_mxC. move: (Ha ((J *m principal_w2 I) 0 0)). apply/contra. rewrite {1}[J *m principal_w2 I]mx11_scalar -scalar_mxM. move/eqP/matrixP => /(_ 0 0). rewrite !mxE /= !mulr1n => ->. by rewrite mulrC. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool Arith.Wf_nat) mathcomp(eqtype ssrnat div seq path) mathcomp(ssralg fintype perm tuple choice generic_quotient) mathcomp(matrix bigop zmodp mxalgebra poly) stronglydiscrete