proposition: Lemma principal_w1_correct : forall n (I : 'cV[R]_n), principal_w1 I *m I = principal I.
proof: Proof. elim => [I | n ih]; first by rewrite flatmx0 mulmx0 /principal rmorph0. rewrite [n.+1]/(1 + n)%nat => I. rewrite -[I]vsubmxK /principal /= col_mxKd {-2}vsubmxK. case: egcdrP => g u v a1 b1 hbezout _ h1 h2 /=. rewrite [row_mx u%:M _ *m _]mul_row_col -scalemxAl ih /principal h2. have -> : usubmx I = (I 0 0)%:M. apply/matrixP => i j. by rewrite !mxE !ord1 eqxx /= mulr1n lshift0. rewrite h1 !scalar_mxM -mul_scalar_mx !mulmxA -mulmxDl -!scalar_mxM -rmorphD. by rewrite hbezout mul1mx. 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