proposition: Lemma BZquo_div1 a b: intp a -> intp b -> b <> \0z -> (BZ_val a) %%c (BZ_val b) = \0c -> a = b *z (a %/z b).
proof: Proof. move => az bz bnz de; rewrite /BZquo - lock /BZquo_int; Ytac0; Ytac0. move: (BZquo_val az bz) => [_ ]; set q := BZ_of_nat _ => [qzp qz]. have pbz: P b <> \0c by move => h; case: bnz; exact (BZ_0_if_val0 bz h). move: (cdivision(BZ_valN az) (BZ_valN bz) pbz)=> [_ _ [aa _]]. have aux: cardinalp (P b *c (P a %/c P b)) by fprops. have Pa: P a = P b *c P q. by rewrite BZ_of_nat_val; move: aa; rewrite de csum0r. case: (BZ_sgv az) => sa; rewrite /int_pp sa; Ytac0. rewrite -(proj2 (BZms_hi_pr (BZms_i az sa))) Pa;case: (BZ_sgv bz) => sb. by rewrite sb; Ytac0; rewrite (BZprod_mp (BZms_i bz sb) qzp). Ytac0; rewrite (BZprod_opp_comm bz qz). have bps: inc b BZps by apply /BZps_iP; split => //; exact (BZp_i bz sb). by rewrite (BZprod_mp (BZopp_positive1 bps) qzp) BZopp_val. rewrite - (BZp_hi_pr (BZp_i az sa)) Pa;case:(BZ_sgv bz) => sb; rewrite sb;Ytac0. move: (BZps_sBZp (BZopp_negative1 (BZms_i bz sb))) => h. by rewrite (BZprod_opp_comm bz qz) (BZprod_pp h qzp) BZopp_val. by rewrite -(BZprod_pp (BZp_i bz sb) qzp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)