proposition: Lemma Bezoutl m n : m > 0 -> {a | a < m & m %| gcdn m n + a * n}.
proof: Proof. move=> m_gt0; case: (egcdnP n m_gt0) => km kn def_d lt_kn_m. exists kn; last by rewrite addnC -def_d dvdn_mull. apply: leq_ltn_trans lt_kn_m. by rewrite -{1}[kn]muln1 leq_mul2l gcdn_gt0 m_gt0 orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)