Z.mod_mul_r and Z.rem_mul_r reversed

[whonore]

Description of the problem

Check Z.mod_mul_r.
(* forall a b c : Z,
     b <> 0 -> c <> 0 -> Z.rem a (b * c) = Z.rem a b + b * Z.rem (a ÷ b) c *)
Check Z.rem_mul_r.
(* forall a b c : Z,
     b <> 0 -> 0 < c -> a mod (b * c) = a mod b + b * ((a / b) mod c) *)

Shouldn't these names be switched to be consistent with Nat.mod_mul_r and N.mod_mul_r, which both have similar conclusions to Z.rem_mul_r?

Coq Version

At least 8.8 - master.