Theorem: Nat.isDvdNat_pos_iff (Logic/Vorspiel/Arith.lean)

State before:
n m : ℕ
⊢ 0 < n.isDvdNat m ↔ n ∣ m
Tactic:
simp[isDvdNat]
State after:
n m : ℕ
⊢ (0 < if n ∣ m then 1 else 0) ↔ n ∣ m

State before:
n m : ℕ
⊢ (0 < if n ∣ m then 1 else 0) ↔ n ∣ m
Tactic:
by_cases n ∣ m <;> simp[*]
State after:
no goals