proposition: Lemma BZdivision_opp_a2 a b: intp a -> intp b -> b <> \0z -> (P a %%c P b) <> \0c -> ( (BZopp a) %%z b <> \0z /\ (BZopp a) %%z b = (BZabs b) -z (a %%z b)).
proof: Proof. move => az bz bnz pz; split. set c := BZopp a; move:(ZSo az) => cz. rewrite /BZrem => ez. have ha: inc (BZopp a %/z b) BZ by apply: ZS_quo. move /(BZdiff_diag_rw cz (ZSp bz (ZS_quo cz bz))): ez => h. move: (f_equal P h); rewrite BZopp_val (BZprod_abs2 bz ha); aw. move: (BZ_valN ha); set q := P _ => qB eq. by move: (cdivides_pr1 qB (BZ_valN bz)) => [_ _]; rewrite - eq. set c := BZabs b. suff: BZopp a %%z c = c -z a %%z c. move => t; case /BZ_i0P: (bz) => bs; last by rewrite - (BZabs_pos bs). by rewrite - (BZrem_opp_b az bz) -( BZrem_opp_b (ZSo az) bz)- (BZabs_neg bs). rewrite /BZrem; set q := (a %/z c). suff: BZopp a %/z c = BZopp (BZsucc q). have bza: intp c by apply: ZSa. have qz: intp q by apply: ZS_quo. have sq1 := (ZSs qz ZS1). move: (ZSp bza qz) => sq2. move => ->. rewrite /BZsucc /BZdiff (BZopp_prod_r bza (ZSo sq1)) (BZopp_K sq1). rewrite (BZoppB az sq2) BZsumC (BZsumA bza sq2 (ZSo az)). by rewrite (BZprodDr bza qz ZS1) (BZprod_1r bza) (BZsumC c). case: (equal_or_not a \0z) => anz. case: pz; rewrite anz BZ0_val. by move: (cdivision_of_zero (BZ_valN bz)) => [ [_ _ ok] _]. have panz: (P a <> \0c) by move =>h; case: anz; exact (BZ_0_if_val0 az h). have cnz: c <> \0z by move => cz; move:(BZabs_0p bz cz). rewrite /q /BZquo -lock /BZquo_int/int_pp (BZabs_sg bz)(BZabs_val b) BZopp_val. set q1:= (BZ_of_nat _). have q1z: intp q1 by apply: BZ_of_nat_i;apply: NS_quo;apply: BZ_valN. move: (ZS_succ q1z) => q2z; move: (ZSo q2z) => q3z. move: (BZabs_sg bz) => hh. do 5 Ytac0. rewrite {1} /BZopp. rewrite /int_pp/int_np; case: (equal_or_not (Q a) C0). move => ->; Ytac0; Ytac0; rewrite /BZ_of_nat; aw; Ytac0. rewrite (BZoppD q3z ZS1) (BZopp_K q2z). rewrite /BZsucc (BZsumC q1) - {1} (BZdiff_sum ZS1 q1z) //. move => qna; case: (BZ_sgv az) => qaa; first by case: qna. by Ytac0; Ytac0; rewrite /BZm_of_nat; Ytac0; aw; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)