proposition: Theorem quot_rem_unique : forall b q1 q2 r1 r2 : t, (0<=r1<b \/ b<r1<=0) -> (0<=r2<b \/ b<r2<=0) -> b*q1+r1 == b*q2+r2 -> q1 == q2 /\ r1 == r2.
proof: Proof. intros b q1 q2 r1 r2 Hr1 Hr2 EQ. destruct Hr1; destruct Hr2; try (intuition; order). - apply NZQuot.div_mod_unique with b; trivial. - rewrite <- (opp_inj_wd r1 r2). apply NZQuot.div_mod_unique with (-b); trivial. + rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto. + rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto. + now rewrite 2 mul_opp_l, <- 2 opp_add_distr, opp_inj_wd. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv