Natural-number lemmas

Auxiliary material for the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; upstreaming candidates for Mathlib.

theorem Nat.eq_and_eq_of_le_of_le_of_mul_eq_mul {a b c d : ℕ} (hac : a ≤ c) (hbd : b ≤ d) (hmul : a * b = c * d) (hc : 0 < c) (hd : 0 < d) : a = c ∧ b = d

If a ≤ c, b ≤ d and a * b = c * d with c, d positive, then a = c and b = d. The positivity hypotheses are needed since ℕ-multiplication is not strictly monotone at 0 (compare mul_eq_mul_iff_eq_and_eq, which does not apply to ℕ).