proposition: Lemma BZgcd_s2 a b (g:= (BZgcd a b)): intp a -> intp b -> [/\ inc g BZ, inc (a %/z g) BZ & inc (b %/z g) BZ].
proof: Proof. by move => az bz; move: (ZS_gcd az bz) => pz; split => //; apply: ZS_quo. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)