proposition: Lemma Bezout_coprimepP p q : reflect (exists u, u.1 * p + u.2 * q %= 1) (coprimep p q).
proof: Proof. rewrite -gcdp_eqp1; apply: (iffP idP)=> [g1|]. by case: (Bezoutp p q) => [[u v] Puv]; exists (u, v); apply: eqp_trans g1. case=> [[u v]]; rewrite eqp_sym=> Puv; rewrite /eqp (eqp_dvdr _ Puv). by rewrite dvdp_addr dvdp_mull ?dvdp_gcdl ?dvdp_gcdr //= dvd1p. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)