proposition: Lemma gdco_kapP (a b c : R) : gcdr a (gcdr b c) %= 1 -> let: (p, q) := gdco_kap a b c in coprimer (p * a) (p * b + q * c).
proof: Proof. rewrite /gdco_kap /=. have [g /= x y z a1 b1 c1] := egcdr3P a b c. move=> Habc1 /eqd_ltrans <- Ha Hb Hc g_eq1. move: Habc1 g_eq1 => /(congr1 ( *%R^~ g)); rewrite !mulrDl mul1r. rewrite -!mulrA -Ha -Hb -Hc {Ha Hb Hc} => <- {g a1 b1 c1}. have [-> | an0 Habc] := eqVneq a 0. rewrite /coprimer !mulr0 add0r => Hbc. by rewrite (eqd_ltrans (gcd0r _)). case: egcdrP => /= g u v a' b' Hab' Hg Hc Hr. move: Hab' Hg => /(congr1 ( *%R^~ g)); rewrite mulrDl mul1r. rewrite -!mulrA -Hc -Hr {Hc Hr} => <- {a' b' g}. rewrite (eqd_rtrans (coprimer_gdco c an0)) => Hu. have: 1 %| 1 - b by rewrite dvd1r. rewrite -(eqd_dvdl _ Hu) /dvdr. case: odivrP => //= k' /(canRL (addrNK _)). rewrite mulrDr !mulrA addrAC !mul1r => Hk' _. rewrite /coprimer; set d := gcdr _ _. have cdc: coprimer d c. apply: gcdr_def; rewrite ?dvd1r // => t td tc. rewrite -(eqd_dvdr _ Habc) -addrA dvdr_add //. by rewrite dvdr_mull ?(dvdr_trans td) /d ?dvdr_gcdl. rewrite -[y * b](@addrNK _ (y * (b + k' * v * c))). rewrite {1}mulrDr opprD addrA subrr sub0r addrAC dvdr_add //; last first. by rewrite dvdr_mull // (dvdr_trans td) /d // dvdr_gcdr. by rewrite !mulrA addrC -mulrBl dvdr_mull. suff dr: d %| gdco c a. by rewrite -dvdr1 Hk' -addrA dvdr_add // /d ?dvdr_gcdr // dvdr_mull. case: gdcoP => /= [a_eq0|r a_neq0 ra crc]; first by rewrite a_eq0 eqxx in an0. by apply => //; rewrite 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