proposition: Lemma coprime_bezout2 a b: coprime a b -> (a = \0c /\ b = \1c) \/ exists u v, [/\ natp u, natp v & a *c u = \1c +c b *c v].
proof: Proof. move=> h. move:(cleR (CS_sum2 a b)). move:(NS_sum (proj31 h)(proj32 h)). move: {1 3}(a +c b) => n nN; move: n nN a b h; apply:Nat_induction. move => a b [aN bN cab] /cle0 /csum_nz [az bz]. set H := cdivides_zero NS0. by rewrite az bz in cab;move: (card1_nz(esym (cab \0c H H))). move => N nN Hrec a b cab /cle_eqVlt; case => ll; last first. by move/(cltSleP nN): ll => ll; apply: Hrec. move:(cab) => [aN bN _]. case: (NleT_ee aN bN) => leab. move: (cdiff_pr leab); move: (NS_diff a bN); set c := _ -c _ => cN bv. case: (equal_or_not a \0c) => anz. left; split => //; move:(proj33 cab); rewrite anz => h. by move: (h b (cdivides_zero bN) (cdivides_itself bN)). right. move: cab; rewrite - bv csumC => /(coprime_diff cN) => cac. have ll1: a +c c <=c N. by apply/(cltSleP nN); rewrite - ll bv csumC;apply:csum_M0lt. case: (Hrec _ _ cac ll1); first by case. move => [u [v [un vN bz]]]; exists (v+c u), v; split;[ fprops | done | ]. by rewrite cprodDl csumA - bz csumC cprodDr. move: (cdiff_pr leab); move: (NS_diff b aN); set c := _ -c _ => cN av. right;case: (equal_or_not b \0c) => bnz. move:(proj33 cab); rewrite bnz => h. rewrite (h a (cdivides_itself aN) (cdivides_zero aN)). exists \1c,\0c; split; [apply: NS1 | apply: NS0 | ]. by rewrite (cprod1r CS1) cprod0r (csum0r CS1). have ll1: c +c b <=c N. by apply/(cltSleP nN); rewrite csumC - ll av; apply:csum_M0lt. move: cab; rewrite -av csumC => /coprime_S/(coprime_diff cN)/coprime_S => cac. case: (Hrec _ _ cac ll1). move => [-> ->]; exists \1c,\0c; split; [exact NS1 | exact NS0 |]. by rewrite (csum0l CS1) (cprod1l CS1) cprod0r (csum0r CS1) . move => [u [v [un vN bz]]]; exists u, (v +c u); split;[ done |fprops | ]. by rewrite cprodDr csumA - bz cprodDl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)