proposition: Lemma principal_w2_correct : forall n (I : 'cV[R]_n), principal_w2 I *m principal I = I.
proof: Proof. move=> n I. rewrite mul_mx_scalar. apply/matrixP => i j; rewrite !mxE !ord1 /= {j}. case: n I i => [|n] I i; first by rewrite !flatmx0 /= mul0r !mxE. case: odivrP => [x -> | H]; first by rewrite mulrC. case/dvdrP: (principal_gen_dvd I i)=> x Hx. move: (H x). by rewrite Hx eqxx. 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