Theorem: Misc.Nat.lt_div_iff_mul_lt (LeanSAT/Util/Misc.lean)

State before:
n d : Nat
hnd : d ∣ n
a : Nat
⊢ a < n / d ↔ d * a < n
Tactic:
rcases d.eq_zero_or_pos with (rfl | hd0)
State after:
case inl
n a : Nat
hnd : 0 ∣ n
⊢ a < n / 0 ↔ 0 * a < n

case inr
n d : Nat
hnd : d ∣ n
a : Nat
hd0 : d > 0
⊢ a < n / d ↔ d * a < n

State before:
case inr
n d : Nat
hnd : d ∣ n
a : Nat
hd0 : d > 0
⊢ a < n / d ↔ d * a < n
Tactic:
rw [← mul_lt_mul_left hd0, ← Nat.eq_mul_of_div_eq_right hnd rfl]
State after:
no goals

State before:
case inl
n a : Nat
hnd : 0 ∣ n
⊢ a < n / 0 ↔ 0 * a < n
Tactic:
simp [zero_dvd_iff.mp hnd]
State after:
no goals