proposition: Lemma coprime_egcdn n m : n > 0 -> coprime (egcdn n m).1 (egcdn n m).2.
proof: Proof. move=> n_gt0; case: (egcdnP m n_gt0) => kn km /= /eqP. have [/dvdnP[u defn] /dvdnP[v defm]] := (dvdn_gcdl n m, dvdn_gcdr n m). rewrite -[gcdn n m]mul1n {1}defm {1}defn !mulnA -mulnDl addnC. rewrite eqn_pmul2r ?gcdn_gt0 ?n_gt0 //; case: kn => // kn /eqP def_knu _. by apply/coprimeP=> //; exists (u, v); rewrite mulnC def_knu mulnC addnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)