proposition: Lemma coprimezP m n : reflect (exists uv, uv.1 * m + uv.2 * n = 1) (coprimez m n).
proof: Proof. apply: (iffP eqP) => [<-| [[u v] /= Duv]]. by exists (egcdz m n); case: egcdzP. congr _%:Z; apply: gcdn_def; rewrite ?dvd1n // => d dv_d_n dv_d_m. by rewrite -(dvdzE d 1) -Duv [m]intEsg [n]intEsg rpredD ?dvdz_mull. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly ssrnum ssrint archimedean rat matrix) mathcomp(polydiv perm zmodp mxalgebra vector)