fact: Fixpoint principal_w1 n : 'cV[R]_n -> 'rV[R]_n := if n is p.+1 then fun (I : 'cV[R]_(1 + p)) => let g := principal_gen (dsubmx I) in let us := principal_w1 (dsubmx I) in let: (g',u,v,a1,b1) := egcdr (I 0 0) g in row_mx u%:M (v *: us) else fun => 0.
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