proposition: Lemma ZpS_quo a b: inc a BZp -> inc b BZp -> inc (a %/z b) BZp.
proof: Proof. move => az bz. move: (BZquo_val (BZp_sBZ az) (BZp_sBZ bz)) => [_]. set q := BZ_of_nat _ => qz _. rewrite /BZquo - lock /BZquo_int; Ytac ra; first by apply: ZpS0. by rewrite /int_pp (BZp_sg az) (BZp_sg bz);Ytac0; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)