proposition: Lemma pid_gdco a b : {r : R & gdco_spec a b r}.
proof: Proof. have [->|b_neq0] := eqVneq b 0; first by exists 0; constructor. elim: (sdvdr_wf b) => {}b _ ihp in b_neq0 *. have [cba|ncba] := boolP (coprimer a b). by exists b; constructor; rewrite ?cpa ?orbT // coprimer_sym. have := dvdr_gcdr a b; case: dvdrP => // [/choice.sig_eqW /= [r b_eq _]]. have := b_neq0; rewrite b_eq mulf_eq0 negb_or => /andP [r_neq0 g_neq0]. have [||r' r_gdco] // := ihp r. by rewrite sdvdr_def b_eq dvdr_mulr //= dvdr_mull_l. case: r_gdco r_neq0 => [->|/= {}r' _ dvdr'r cr'q r'P r_neq0]. by rewrite eqxx. exists r'; constructor; rewrite ?dvdr_mulr // -?b_eq //=. move=> d dp cdq; apply: r'P => //. rewrite -(@euclid _ (gcdr a b)) -?b_eq //. exact: coprimer_dvdr (dvdr_gcdl _ _) _. 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