proposition: Lemma coprimeP n m : n > 0 -> reflect (exists u, u.1 * n - u.2 * m = 1) (coprime n m).
proof: Proof. move=> n_gt0; apply: (iffP eqP) => [<-| [[kn km] /= kn_km_1]]. by have [kn km kg _] := egcdnP m n_gt0; exists (kn, km); rewrite kg addKn. apply gcdn_def; rewrite ?dvd1n // => d dv_d_n dv_d_m. by rewrite -kn_km_1 dvdn_subr ?dvdn_mull // ltnW // -subn_gt0 kn_km_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)