proposition: Theorem mod_unique: forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> r == a mod b.
proof: Proof. intros a b q r Ha (Hb,Hr) EQ. destruct (div_mod_unique b q (a/b) r (a mod b)); auto. - apply mod_bound_pos; order. - rewrite <- div_mod; order. Qed.
imports: NZAxioms NZMulOrder