proposition: Lemma BZ_coprime_if_Bezout a b: intp a -> intp b -> BZBezout a b -> BZcoprime a b.
proof: Proof. move => az bz [x [y [xz yz etc]]]; red; symmetry. apply:(BZ_gcd_unq az bz (BZps_sBZp ZpsS1)). set_extens t. move => /funI_P [z zz]; rewrite (BZprod_1l zz) => ->. move: (ZSp xz zz)(ZSp yz zz) => pa pb. apply /Zo_P;split => //; exists (x *z z);exists (y *z z);split => //. rewrite (BZprodA az xz zz) (BZprodA bz yz zz). by rewrite - (BZprodDl zz (ZSp az xz)(ZSp bz yz)) etc BZprod_1l. move => /Zo_P [tz _]; apply /funI_P; ex_tac; symmetry;exact (BZprod_1l tz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)