proposition: Theorem mod_unique: forall a b q r, 0<=r<abs b -> a == b*q + r -> r == a mod b.
proof: Proof. intros a b q r Hr EQ. assert (Hb : b~=0). { pos_or_neg b. - rewrite abs_eq in Hr; intuition; order. - rewrite <- opp_0, eq_opp_r. rewrite abs_neq' in Hr; intuition; order. } destruct (div_mod_unique b q (a/b) r (a mod b)); trivial. - now apply mod_always_pos. - now rewrite <- div_mod. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv