proposition: Lemma minimal_bezout a b: 0 < a -> 0 < b -> coprime a b -> exists u v, [/\ u * a = v * b + 1, v < a & u <= b].
proof: Proof. move => ap bp cab; move/(coprimeP b ap): cab => [p hp]. have : p.1 * a = p.2 * b + 1. by move: (ltnSn 0); rewrite -{2 3} hp subn_gt0 => /ltnW h; rewrite subnKC. rewrite (divn_eq p.2 a) mulnDl mulnAC -addnA => sa. have la: p.2 %/ a * b <= p.1 by rewrite -(leq_pmul2r ap) sa leq_addr. move/eqP:sa; rewrite -{1} (subnKC la) mulnDl eqn_add2l => /eqP hc. have va:= (ltn_pmod p.2 ap). move: (va);rewrite -(ltn_pmul2r bp) -addn1- hc mulnC (leq_pmul2l ap) => hd. by exists (p.1 - p.2 %/ a * b), (p.2 %% a). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)