proposition: Lemma BZgcd_prop2 a b: intp a -> intp b -> (exists x y, [/\ intp x, intp y & (BZgcd a b = (a *z x) +z (b *z y))]).
proof: Proof. move => az bz; move: (BZgcd_prop1 az bz) => [pa pb]. by move: (BZ_in_ideal4 (BZp_sBZ pa)) => [_]; rewrite pb => /Zo_P [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)