proposition: Theorem Zdiv_mod_unique b q1 q2 r1 r2 : 0 <= r1 < Z.abs b -> 0 <= r2 < Z.abs b -> b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2.
proof: Proof. intros Hr1 Hr2 H. rewrite <- (Z.abs_sgn b), <- !Z.mul_assoc in H. destruct (Z.div_mod_unique (Z.abs b) (Z.sgn b * q1) (Z.sgn b * q2) r1 r2); auto. split; trivial. apply Z.mul_cancel_l with (Z.sgn b); trivial. rewrite Z.sgn_null_iff, <- Z.abs_0_iff. destruct Hr1; Z.order. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms