proposition: Lemma BZ_Bezout_if_coprime a b: intp a -> intp b -> BZcoprime a b -> BZBezout a b.
proof: Proof. move => az bz; move:(BZgcd_prop2 az bz) => [x [y [xz yz ha]]] hb. by exists x,y; split => //; rewrite /Bezout_rel - ha. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)