proposition: Lemma BZ_coprime1r a: intp a -> BZcoprime a \1z.
proof: Proof. move: ZS1 ZS0=> oz zz az;apply (BZ_coprime_if_Bezout az oz). by exists \0z, \1z; rewrite /Bezout_rel BZprod_0r BZprod_1r // BZsum_0l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)