qify should use divisibility hypotheses on nats

[timotree3]

Right now, qify seems to be able to use divisibility hypotheses on ints but not nats. It would be nice if it worked for both.

import Mathlib.Tactic.Qify

example (n m : ℕ) (h : m ∣ n): n / m * m = n := by
  qify [h]
  -- oops! h wasn't used. goal is:
  -- ⊢ ↑(↑n / ↑m) * ↑m = ↑n
  sorry

example (n m : ℕ) (h : m ∣ n): n / m * m = n := by
  rw [← Int.ofNat_dvd] at h
  qify [h]
  -- yay! h was used. goal is:
  -- ⊢ ↑n / ↑m * ↑m = ↑n
  sorry

[timotree3]

In turns out this is a confluence issue in the simp set that qify uses:

import Mathlib.Algebra.CharZero.Lemmas
import Mathlib.Tactic.Qify

example (n m : ℕ) (h : m ∣ n): n / m * m = n := by
  -- qify [h] is equivalent to the following simp here:
  simp (config := { decide := false }) only [Mathlib.Tactic.Zify.nat_cast_eq, Nat.cast_mul, Int.ofNat_ediv,
    Mathlib.Tactic.Qify.int_cast_eq, Int.cast_mul, Int.cast_ofNat]
  -- oops! h wasn't used. goal is:
  -- ⊢ ↑(↑n / ↑m) * ↑m = ↑n
  sorry

example (n m : ℕ) (h : m ∣ n): n / m * m = n := by
  -- if we remove a lemma, it works!
  simp (config := { decide := false }) only [Mathlib.Tactic.Zify.nat_cast_eq, Nat.cast_mul, --Int.ofNat_ediv,
    Mathlib.Tactic.Qify.int_cast_eq, Int.cast_mul, h, Nat.cast_div_charZero, Int.cast_ofNat]
  -- yay! h was used. goal is:
  -- ⊢ ↑n / ↑m * ↑m = ↑n
  sorry