proposition: Lemma adequate_gdco a b r : adequate_spec a b r -> gdco_spec a b r.
proof: Proof. move=> [->|]; first by constructor => //; rewrite eqxx. move=> {}r b_neq0 dvd_rb cra /= Hs; constructor=> //=. move=> /= d dvd_db cda; have [du|dnu] := boolP (d \is a GRing.unit). by rewrite dvdUr ?eqd1. case: dvdrP dvd_rb => // [[s ->]] _ in Hs dvd_db *. rewrite -(@euclid _ s) // /coprimer 1?mulrC // -unitd1. apply: (contraLR (Hs _ _)); first by rewrite dvdr_mul // dvdr_gcdr. rewrite /coprimer -(eqd_ltrans (gcdrA _ _ _)). exact: coprimer_dvdr (dvdr_gcdr _ _) _. 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