nat_abs vs lifted nat

Stream: new members

[Will Midwood]

Hi there,
In one of my theorems, I have arrived needing to solve this goal:

x y : ℤ,
e : ℕ,
hex : e ∣ x.nat_abs,
hey : e ∣ y.nat_abs
⊢ ↑e ∣ x ∧ ↑e ∣ y

This seems like I need to switch between types, but I'm not exactly sure how to do that.

[Will Midwood]

Thanks in advance ^

[Ruben Van de Velde]

There's a lemma in mathlib that says exactly this, try split, library_search

[Ruben Van de Velde]

Will probably be called something like int.dvd_nat_abs

[Ruben Van de Velde]

Ah, no. It's docs#int.coe_nat_dvd_left