PNat.dvd_iff

Stream: mathlib4

[Kevin Buzzard]

theorem dvd_iff {k m : ℕ+} : k ∣ m ↔ (k : ℕ) ∣ (m : ℕ) := by

If this were the other way around it could be a norm_cast lemma, and then norm_cast would be able to remove those up-arrows (which I just wanted it to do I had a hypothesis  ↑D ∣ ↑M). But it looks like it's mostly rewritten forwards. Can I add the backwards one and tag it? Or is there another trick? I prefer a tactic rather than having to remember the name of a lemma.

[Yaël Dillies]

You can tag it with @[norm_cast] already. norm_cast is smart

[Yaël Dillies]

But I agree it should be turned around regardless

[Kevin Buzzard]

norm_cast: badly shaped lemma, lhs must contain at least one coe
  k ∣ m

'swhy I asked

[Yaël Dillies]

Hmm, it used to work in Lean 3