fact: Fixpoint Bareiss_rec m a : 'M[R]_(1 + m) -> R := if m is p.+1 return 'M[R]_(1 + m) -> R then fun (M: 'M[R]_(1 + _)) => let d := M 0 0 in let l := ursubmx M in let c := dlsubmx M in let N := drsubmx M in let M' := d *: N - c *m l in let M'' := dvd_step a M' in Bareiss_rec d M'' else fun M => M 0 0.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly polydiv mxpoly) ssrcomplements dvdring minor atomic_operations