proposition: Lemma minimal_bezout_prop a b u v: u * a = v * b + 1 -> v < a -> u <= b -> (forall u' v', u' * a = v' * b +1 -> (u <= u') && (v <= v')).
proof: Proof. move => B ua vb u' v' B'. have ap: 0 < a by move:ua; case:(a). case (posnP b) => bp. by move: vb B; rewrite bp leqn0 => /eqP ->; rewrite muln0. case: (ltnP u' u) => cp; last first. by rewrite -(leq_pmul2r bp) -(leq_add2r 1) -B' - B (leq_pmul2r ap) cp. have cp2:=(ltnW cp). have cp1: v' <= v. by rewrite - (leq_pmul2r bp)-(leq_add2r 1) -B -B' (leq_pmul2r ap). move /eqP: B; rewrite -(subnK cp1) -(subnK cp2) !mulnDl - addnA -B'. rewrite eqn_add2r; set x := (u - u'); set y := (v - v') => /eqP eq3. have cap: coprime b a by rewrite coprime_sym; apply:(coprime_if_bezout B'). have eq4: x = (x %/ b) * b. symmetry; apply /eqP; rewrite - (dvdn_eq b x). by move:(Gauss_dvdr x cap); rewrite mulnC eq3 {1}/dvdn modnMl eqxx => <-. case: (posnP u') =>uz; first by move/eqP: B'; rewrite uz addn1. have: u < b + u' by apply: (leq_ltn_trans vb); rewrite ltn_paddr. rewrite -(subnK cp2) -/x eq4 ltn_add2r -{3}(mul1n b) ltn_pmul2r // ltnS leqn0. by move => /eqP qp; move: (ltn_eqF cp); rewrite -(subnK cp2) -/x eq4 qp eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)