fact: Definition hermite (M : 'M[R]_2) := Bezout_step (M 0 0) (M 1 0) M 0.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype matrix mxalgebra bigop zmodp perm choice) dvdring mxstructure minor stronglydiscrete coherent edr