proposition: Lemma BZgcd_x1 x: intp x -> BZgcd x \1z = \1z.
proof: Proof. move: ZS0 ZS1=> z0 z1 h; symmetry. apply: (BZ_gcd_unq h ZS1 (BZps_sBZp ZpsS1)). set_extens t. move /funI_P => [z zz ->]; apply/Zo_P; split; first by rewrite (BZprod_1l zz). by exists \0z, z; split => //; rewrite BZprod_0r BZprod_1l // BZsum_0l. move => /Zo_P [tZ [u [v [uz vz ->]]]]. set w := (x *z u +z \1z *z v). have wz: inc w BZ by apply:ZSs; apply: ZSp. by apply/funI_P; ex_tac; rewrite BZprod_1l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)