proposition: Lemma BZquo_opp_b a b: intp a -> intp b -> a %/z (BZopp b) = BZopp (a %/z b).
proof: Proof. move => az bz. case: (equal_or_not b \0z) => bn0. by rewrite bn0 BZopp_0 BZ_quo0 BZopp_0. have bon0: BZopp b <> \0z by dneg xx; move: (BZopp_K bz); rewrite xx BZopp_0. rewrite /BZquo - lock /BZquo_int; Ytac0; Ytac0; rewrite BZopp_val. move: (BZquo_val az bz) => [_ _]; set q := BZ_of_nat _ => qzp. move: (BZopp_sg bz bn0) => [aux1 aux2]. case: (equal_or_not (Q b) C0) => ha. rewrite/int_pp (aux1 ha) ha; Ytac0; Ytac0; Ytac0; Ytac0; Ytac0; Ytac0. by Ytac hb; Ytac0; [symmetry;apply: BZopp_K | Ytac hc; Ytac0]. case: (BZ_sgv bz); [ by done | move => bp]. rewrite /int_pp (aux2 bp); do 6 Ytac0; Ytac pc; Ytac0 => //. by Ytac pd; Ytac0 => //;rewrite BZopp_K //; apply: ZS_succ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)