proposition: Lemma coprime_bezout1 a b: natp a -> natp b -> (exists u v, [/\ natp u, natp v & a *c u = \1c +c b *c v]) -> coprime a b.
proof: Proof. move => aN bN [u [v [uN vN eq1]]]; split => // x xda xdb. move:(cdivides_trans2 uN xda); rewrite eq1 csumC => xdc. move: (cdivides_diff1 NS1 (cdivides_trans2 vN xdb) xdc). apply:cdivides_oner. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)