feat: generalize fract_div_intCast_eq_div_intCast_mod

[mo271]

---

[github-actions]

PR summary 76507f175f

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Order.Floor	603	609	+6 (+1.00%)

Import changes for all files

Files	Import difference
Mathlib.Order.Filter.AtTopBot.Floor	5
5 files Mathlib.Algebra.ContinuedFractions.Computation.Translations Mathlib.Algebra.Order.Floor Mathlib.Algebra.ContinuedFractions.Computation.Basic Mathlib.Data.Int.Log Mathlib.Algebra.Order.Nonneg.Floor	6

---

Declarations diff

+ fmod_nonpos
+ fract_div_intCast_eq_div_intCast_fmod
+ fract_eq_zero_iff
+ lt_fmod_of_pos

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type
5027	-2	porting notes

Current commit 76507f175f
Reference commit 496527772a

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mo271]

TODO Generalise this to allow `n : ℤ` using `Int.fmod` instead of `Int.mod`.`

was added in leanprover-community/mathlib3#17321 by @ocfnash

[mo271]

https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/basic.20facts.20for.20.60fmod.60.20for.20negative.20second.20argument

[mo271]

closing in favor of #19652