proposition: Lemma BZ_positive_quo_gcd a b: inc a BZp -> intp b -> inc (a %/z (BZgcd a b)) BZp.
proof: Proof. move => azp bz; apply:ZpS_quo => //; apply: (ZpS_gcd (BZp_sBZ azp) bz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)