proposition: Lemma BZgcd_div2 a b: intp a -> intp b -> BZgcd a b %|z a.
proof: Proof. move => aZ bZ. move:(BZgcd_div aZ bZ) => [ ha _]; rewrite {2} ha. move: (ZS_gcd aZ bZ) => hb; move: (ZS_quo aZ hb) => hc. apply: (BZdvds_pr1' hc (ZS_gcd aZ bZ)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)