proposition: Lemma BZdvd_correct a b: intp a -> intp b -> b <> \0z -> [/\ inc (a %/z b) BZ, inc (a %%z b) BZp & (BZdivision_prop a b (a %/z b) (a %%z b))].
proof: Proof. move => az bz bnz. pose aux a b := a %%z b <z BZabs b /\ inc (a %%z b) BZp. suff: aux a b. move: (ZS_quo az bz) => qz [pa pb]; split => //; split => //. by rewrite /BZrem (BZsum_diff (ZSp bz qz) az). have Ha: forall a b, inc a BZp -> inc b BZps -> aux a b. move => u v up /BZps_iP [vp vnz]. rewrite /aux (BZabs_pos vp) /BZrem. move: (BZp_sBZ vp) (BZp_sBZ up) => vz uz. set q := (u %/z v). suff: (u <z v *z (q +z \1z) /\ v *z q <=z u). move => [pa pb]. move: (proj31 pb) => pz. move:(ZS_diff (proj32 pb) pz) => rz. split; last by apply /(zle_diffP pz uz). apply /(BZsum_lt2r rz vz pz); rewrite BZsumC (BZsum_diff pz uz). by move: pa; rewrite (BZprodDr vz (ZS_quo uz vz) ZS1) BZsumC BZprod_1r. have: q = u %/z v by done. rewrite /BZquo - lock /BZquo_int (Y_true (BZp_sg up)) (Y_true (BZp_sg vp)). rewrite (Y_false vnz) => ->. move: (BZ_valN (BZp_sBZ up)) (BZ_valN (BZp_sBZ vp)) => pa pb. have pc: P v <> \0c by move => h; case: vnz; exact (BZ_0_if_val0 vz h). move: (cdivision pa pb pc). clear q; set q := (P u %/c P v); set r := (P u %%c P v). move => [qB rB [dp mp]]; move: (BZ_of_natp_i qB) => qzb. move /BZps_iP: ZpsS1 => [bz1p _]. split. rewrite (BZsum_pp qzb bz1p) /BZ_one !BZ_of_nat_val. rewrite (BZprod_pp vp (BZ_of_natp_i (NS_sum qB NS1))) BZ_of_nat_val. apply /(zlt_P1 up). by apply: BZ_of_natp_i;rewrite -/(natp _); fprops. rewrite BZ_of_nat_val dp cprodDr (cprod1r (CS_nat pb)). rewrite csumC (csumC _ (P v)); exact:(csum_Mlteq (NS_prod pb qB) mp). have ppb: inc (P v *c q) Nat by apply:NS_prod. rewrite (BZprod_pp vp (BZ_of_natp_i qB)) BZ_of_nat_val. apply /(zle_P1 _ up); first by apply: BZ_of_natp_i. by rewrite BZ_of_nat_val dp; apply:(Nsum_M0le _ ppb). have Hb: forall a b, inc a BZp -> intp b -> b <> \0z -> aux a b. move => u v => up vp vnz. case /BZ_i1P: vp; [by done | by move => h; apply: Ha | ]. move => vm; move: (BZopp_negative1 vm) => ovp. move: (BZrem_opp_b (BZp_sBZ up) (BZms_sBZ vm)) => e1. by move: (Ha _ _ up ovp); rewrite /aux e1 BZabs_opp. case /BZ_i0P: (az); last by move => h;apply: Hb. move => ams; move: (BZopp_negative1 ams) => oap. move: (Hb _ _ (BZps_sBZp oap) bz bnz) => [pa pb]. case: (equal_or_not ((P a) %%c (P b)) \0c) => de. move: (BZrem_div1 az bz bnz de) => rz. rewrite /aux rz;split ; [ exact : (BZabs_positive bz bnz) | apply: ZpS0 ]. move: (BZdivision_opp_a2 az bz bnz de) => [r2 r1]. move: pa pb r2; rewrite /aux r1; set X := _ %%z _; set bb := BZabs b. have Xp: inc X BZ by apply: ZS_rem. move: (ZSa bz) => abz. move => pa pb pc; split. apply /(zlt_diffP Xp abz); apply /BZps_iP; split => // => e1. move /(zlt_diffP (ZS_diff abz Xp) abz) : pa. by rewrite /BZdiff BZoppB // BZsum_diff //; move /BZps_iP => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)