proposition: Lemma ZS_quo a b: intp a -> intp b -> intp (a %/z b).
proof: Proof. move => az bz; rewrite /BZquo - lock /BZquo_int. move: (BZquo_val az bz) => [_ _]; set q := BZ_of_nat _ => qz. move: (ZSo qz) (ZS_succ qz) ZS0=> oqz sqz z0. by Ytac ra => //; Ytac rb; Ytac rc => //; Ytac rd => //; apply:ZSo. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)