proposition: Lemma coprimerP (a b : R) : reflect (exists xy, xy.1 * a + xy.2 * b = 1) (coprimer a b).
proof: Proof. case: (egcdrP a b) => g u v a1 b1 h1 h2 h3 h4. apply: (iffP idP)=> [/(eqd_trans h2) | [[x y]]] /=. rewrite -unitd1; case/unitrP=> x [hx1 hx2]; exists (x*u,x*v). by rewrite -!mulrA -mulrDr h3 h4 !mulrA -mulrDl h1 mul1r. rewrite {1}h3 {1}h4 !mulrA -mulrDl=> H; move: (@unitr1 R). rewrite -H unitrM !unitd1=> /andP [_ H']. by rewrite /coprimer eqd_sym (eqd_trans _ h2) // eqd_sym. 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