proposition: Lemma Bezout_eq1_coprimepP p q : reflect (exists u, u.1 * p + u.2 * q = 1) (coprimep p q).
proof: Proof. apply: (iffP idP)=> [hpq|]; last first. by case=> [[u v]] /= e; apply/Bezout_coprimepP; exists (u, v); rewrite e eqpxx. case/Bezout_coprimepP: hpq => [[u v]] /=. case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0] e. exists (c2^-1 *: (c1 *: u), c2^-1 *: (c1 *: v)); rewrite /= -!scalerAl. by rewrite -!scalerDr e scalerA mulVf // scale1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)