proposition: Lemma principal_gen_dvd : forall n (I : 'cV[R]_n) i, principal_gen I %| I i 0.
proof: Proof. elim => [I i| n ih]; first by rewrite flatmx0 /= !mxE dvdrr. rewrite [n.+1]/(1 + n)%nat => I i. rewrite -[I]vsubmxK !mxE. case: splitP => j hj /=. rewrite !ord1 !mxE /=. case: splitP => // j' _. rewrite ord1 mxE lshift0. case: egcdrP => g u v a b _. rewrite eqd_def; case/andP => h _ _ _. exact: (dvdr_trans h (dvdr_gcdl _ _)). case: egcdrP => g u v a b _. rewrite eqd_def col_mxKd; case/andP => h _ _ _. apply/(dvdr_trans (dvdr_trans h (dvdr_gcdr _ _))). by rewrite ih. 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