proposition: Lemma krull1_gdcoP a b : gdco_spec a b (krull1_gdco a b).
proof: Proof. rewrite /krull1_gdco; case: (krull1_adequate a b)=> r hr /=. exact: adequate_gdco. Qed.
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