proposition: Theorem mod_unique: forall a b q r, (0<=r<b \/ b<r<=0) -> a == b*q + r -> r == a mod b.
proof: Proof. intros a b q r Hr EQ. assert (Hb : b~=0) by (destruct Hr; intuition; order). destruct (div_mod_unique b q (a/b) r (a mod b)); trivial. - destruct Hr; [left; apply mod_pos_bound|right; apply mod_neg_bound]; intuition order. - now rewrite <- div_mod. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv