proposition: Lemma gdco_adequate a b r : gdco_spec a b r -> adequate_spec a b r.
proof: Proof. move=> [|/= {}r b_neq0 rb cra Hd]; first by constructor. constructor => //= d dr_dvd_b; apply: contra => cda. case: dvdrP rb => [[s ->]|//] {b} _ in Hd dr_dvd_b b_neq0 *. have r_neq0 : r != 0 by move: b_neq0; rewrite mulf_eq0 negb_or => /andP []. have := Hd _ dr_dvd_b. rewrite -[r as X in _ %| X]mul1r dvdr_mul2r // dvdr1 unitd1; apply. by rewrite coprimer_mull cra cda. 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