proposition: Lemma BZdvd_unique a b q r q' r': intp a -> intp b -> b <> \0z -> intp q -> intp r -> intp q' -> intp r' -> BZdivision_prop a b q r -> BZdivision_prop a b q' r' -> (q = q' /\ r =r').
proof: Proof. move => az bz qnz; move: q r q' r'. have alt:forall q r, inc q BZ -> inc r BZ -> BZdivision_prop a b q r -> [/\ (b *z q) <=z a, a <z (b *z ((BZsign b) +z q)) & r = a -z (b *z q)]. move => q r qz rz. move: (ZSp bz qz) (ZS_sign b) => qa qb. have qc: b *z (BZsign b +z q) = b *z q +z BZabs b. by rewrite (BZprodDr bz qb qz) BZsumC (BZsign_abs bz). move: (BZsum_lt2l rz (ZSa bz) qa) => qd. move => [pa pb pc];split => //. by rewrite pa; apply: BZsum_Mp. by rewrite qc pa; apply /qd. by rewrite pa BZdiff_sum. move => q r q' r' qz rz q'z r'z h h'. move: (alt _ _ qz rz h) => [pa pb pc]. move: (alt _ _ q'z r'z h') => [pa' pb' pc']. suff: q = q' by move => sq; rewrite pc pc' sq. move: (ZS_sign b) => ab. have aux: forall q q', inc q BZ -> inc q' BZ -> b *z q' <z b *z (BZsign b +z q) -> inc (b *z (BZsign b +z (q -z q'))) BZps. move => z z' zz z'z le. move: (ZSs ab zz) => sa. move /(zlt_diffP (ZSp bz z'z) (ZSp bz sa)): le. by rewrite - (BZprodBr bz sa z'z) /BZdiff (BZsumA ab zz (ZSo z'z)). have aux2: forall q q', inc q BZ -> inc q' BZ -> inc (\1z +z (q -z q')) BZps -> q' <=z q. move => z z' zz z'z le;apply /(zlt_succ1P z'z zz). apply /(zlt_diffP z'z (ZS_succ zz)). by rewrite /BZsucc /BZdiff (BZsumC z) - (BZsumA ZS1 zz (ZSo z'z)). have aux3: forall q q', inc q BZ -> inc q' BZ -> inc (\1mz +z (q -z q')) BZms -> q <=z q'. move => z z' zz z'z le; move: (BZopp_negative1 le). rewrite (BZoppD ZSm1 (ZS_diff zz z'z)). by rewrite (BZoppB zz z'z) BZopp_m1; apply: aux2. have r1: b *z q <z b *z (BZsign b +z q') by BZo_tac. have r2: b *z q' <z b *z (BZsign b +z q) by BZo_tac. move: (aux _ _ qz q'z r2) (aux _ _ q'z qz r1) => r3 r4. move: (BZps_stable_prod1 bz (ZSs ab (ZS_diff qz q'z)) r3). move: (BZps_stable_prod1 bz (ZSs ab (ZS_diff q'z qz)) r4). case /BZ_i1P: bz => ha //. move=> [s1 s2] [s3 s4]. move/s1: (ha); move/s3: (ha); rewrite (BZsign_pos ha) => s5 s6. move: (aux2 _ _ qz q'z s5) (aux2 _ _ q'z qz s6) => l1 l2; BZo_tac. move=> [s1 s2] [s3 s4]. move/s2: (ha); move/s4: (ha); rewrite (BZsign_neg ha) => s5 s6. move: (aux3 _ _ qz q'z s5) (aux3 _ _ q'z qz s6) => l1 l2; BZo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)